Tag Info

New answers tagged

1

Consider the inverse: that there exists an integer $m$ where the smallest factor $n$ is not prime. If that is the case then there exists a prime integer $k$ such that $k < n$ and $k$ divides $n$, thus $k$ also divides $m$, which is a contradiction.


0

Not really a good "strict" proof, if you ask me. For example, you just assumed that $r\implies \neg q$ is true, I see no reason why I should (strictly speaking) believe that.


0

I think there should be some more precision regarding definitions. For instance, the statement "$p$ is prime" is equivalent to saying: For every pair $a,b$ of integers such that $p$ divides $ab$, one of $a$ or $b$ is divisible by $p$. I don't see how this was involved in your proof. Alternatively, you could use the definition of irreducibility and ...


2

Here are three in the order of the bullets above. Note that the quantifiers do cause some issues, especially in #1, but I think these meet the spirit of the question. I am not sure they are accessible to a layman, though. If $A$ is a closed set of real numbers then if $(x_n)$ is a Cauchy sequence in $A$ then $\lim x_n$ is in $A$. Converse: If every Cauchy ...


1

I wonder if Schoenfield has the Hilbert-Bernays metamathematical finitism program in mind. If so, the "finitary" bit is meant at the syntactic level (formalisation of proofs), whereas the semantic content could be anything, including classical (nonconstructive) mathematics.


1

For example we can prove the Fermat last theorem by writing down every instance and checking it numerically. This is not finitary.


0

Hint: $\lnot p \lor \lnot q$ (premise) $\quad |\text{Assume}\; p\land q\;$ (Assumption) $\quad |\;p\;$ ("conjunction elimination") $\quad |\; q\;$ (simplification of conjunction elimination) $\quad |\;\;\vdots $ $\quad | \;\underline{\text{Deduce a contradiction.}}$ Conclude, given the contradiction, that $\lnot(p\land q)$.


2

On the left side \[ \begin{array}{c|c|c|c} p & q & r & p\rightarrow q & p\land (p\rightarrow q )\land r\\ \hline 0 & 0 & 0 & 1 & 0 \\ \hline 0 & 0 & 1 & 1 & 0 \\ \hline 0 & 1 & 0 & 1 & 0 \\ \hline 0 & 1 & 1 & 1 & 0 \\ \hline 1 & 0 & 0 & 0 & 0 \\ \hline 1 & 0 ...


1

For the sake of this answer, we'll fix some theory $T$, which could be $\mathsf{(ZF-Inf)} + \neg \mathsf{Con(ZF-Inf)}$, and "provable" in both senses always means "from the axioms of $T$". We'll also fix some (nonstandard) model $M$ of $T$. There is a distinction between the "real" provability relation, $T \vdash \phi$, and the formalized provability ...


0

Assuming the question is: "Suppose that $A$ is many-one reducible to $B$. Is $A$ polytime many-one reducible to $B$?" The answer is no. The language $\{\Phi : \Phi\text{ valid boolean formula with quantifiers}\}$ is $\mathsf{PSPACE}$-complete (sometimes known as QBF or TQBF). One can many-one reduce this language to the language $\{(G,s,t) : G \text{ ...


3

Method/Algorithm: Break it down into pieces. There are just three variables, $p, q, r$. First start with assigning all possible combinations of truth values to these variables. Then start with other pieces. I would go in the following order. $$ p \to q $$ $$ p \lor q $$ $$ p \land (p \to q) \land r $$ $$ (p \lor q) \to r $$ Now you have all you need ...


2

The usual answer (or dodge, depending on yuor philosophical position) is to talk about the intended model of the natural numbers. If such a thing exists (and many mathematicians do believe it exists, including the constructivist Errett Bishop), then one can interpret references to "finite" at the meta-level as referring to things equinumerable with ...


1

As André Nicolsas commented, all primitive recursive functions are total recursive -- and all total recursive functions are in particular partial recursive. Here "partial" is the less demanding condition. A "partial recursive" function is allowed to but not required to be undefined for some inputs.


1

Sequent proofs should write themselves without you having to think about them (which is the the point of using them!). Think where you want to end up and work backwards (or rather upwards: write the sequent you want to prove at the bottom, and construct the tree from bottom to top ...). You want to establish the sequent $$\Rightarrow A\to (B\to C) \to ...


0

A "long" comment. You can use this example to "format" the sequent calculus axiom and rules : $${ \quad \over \Gamma, A \implies A, \Delta } \, \text{(Axiom)}$$ $${ \Gamma \implies A \quad B \implies \Delta \over \Gamma \implies A \rightarrow B, \Delta } \, \text{(Rule)}$$


0

I think there's a simpler example, that doesn't make reference to the example in Mendelson - I hope somebody can confirm this. Consider this formula interpreted wrt. the theory of the Natural numbers ($T_{\mathbb{N}}$) $T_{\mathbb{N}}\vdash \exists y\forall x. x >= y$ is valid. However, the Skolem equivalent $T_{\mathbb{N}}\cup{\{f\}}\vdash\forall x. ...


0

What you've called "rule" is usually called "axiom" or "axiom scheme" and "identities" are usually called "rules". $A \Rightarrow A, B, C$ (axiom) and $A, B \Rightarrow B, C$ (axiom) implies $A, A\rightarrow B \Rightarrow B, C$ by the second rule. 1 and $A, A\rightarrow B, C \Rightarrow C$ (axiom) implies $A, A\rightarrow B, B\rightarrow C \Rightarrow C$ ...


0

We know that a conditional statement is invalid if it is possible that the antecedent is true and the consequent is false. The following example would show that the proposition you stated is not valid. Let $A(x)$ be a predicate for "x is a square with perimeter equidistant from its center" and $B(x)$ be a predicate for "x is a contradictory object". Then ...


1

The first formula fails when, for every $x$, both $A(x)$ and $B(x)$ are false. In this case the first part holds and the second part does not. A note on this: an implication is always true when its antecedent is false, which is slightly counterintuitive to humans since this conveys no useful information. For example: "my name is Carl implies $1 = 0$" is a ...


1

Yes, your guess about kinds is correct. According to Types and Programming Languages, kinds are "the types of types". From the same source: [...] we introduce a system of kinds that classify type expressions according to their arity, just as arrow types tell us about the arities of terms. Kinds, then, are “the types of types.” In essence, the system ...


1

The two sentences can't both be true; if 1 is true then 2 is false, and if 2 is true then 1 is false. If 1 is true, then we can tell whether a given sentence $\phi$ is valid by asking whether $\lnot \phi$ is satisfiable. So only one of the sentences can be true, and as the first part of the question says, the correct one is #2: the set of valid formulas is ...


3

The "standard" semantics for first-order logic does not allow for interpetations with empty domains. But there other approachs : see Free Logic Regarding Ex 1 : $∀x¬Rxx$, if we stay with the usual approach (no empty domain), we still have an interpretation with a sinle element. Consider the interpretation $\mathfrak A$ with domain $A = \{ 1 \}$ and ...


2

Here's another example: (A) If I hit my thumb with a hammer, then my thumb hurts. If I'm in a reality where I don't hit my thumb with a hammer and my thumb doesn't hurt, I'd still consider (A) to be true.


1

We can take benefit of Kleene's fundamental result (1943) : Kleene’s theorem : A set is recursive if and only if both it and its complement are recursively enumerable. Consider the set $A$ which is the range of the increasing recursive function $f$; this means that $A = \{ a_n : a_n = f(n) \}$, i.e. $A$ is "listed" running the computation of $f$. ...


0

Suppose that : we realize that the theory $T$ has to be consistent, which means that formula $\varphi_1$ that expresses consistency of the theory $T$ is true. This would mean that every model will satisfy $\varphi_1$. It is not clear from the above discussion the "intended meaning" of : "the method of infinitely many deduction steps", unless you are ...


0

Will try to answer my own question (to be updated a future day). Words in ML programmer's guide to ATS (cs.likai.org), suggests a sort is indeed a category above types: Type definition assigns a static identifier to a static expression with the sort "type" […] The only difference is that typedef ensures that t will end up having the "type" sort, ...


4

No. Not at all. If a language has Godel numbering (and certainly the language of set theory with only $\in$ has that), then asserting that a theory in that language is consistent is a number theoretic statement. Namely, it's a statement about integers. Of course, we need to assume that the numbers encoding the axioms of the theory make a definable set of ...


3

Your completion of the last row is not correct: from the given information, $A\otimes B$ could be either true or false. In the last row each of your four conditions (two introduction, two elimination) has at least one false premise (either $A$ or $B$), so no conclusion can be drawn: whatever value you give to $A\otimes B$, there will be no inconsistency. ...


2

The compactness theorem gives many ways to generate theorems of the form "if all finite $X$s have property $P$, then so do all infinite $X$s". A random example from Bell and Slomson Models and Ultraproducts: Let $B$ be an infinite set of boys each of whom has at most a finite number of girlfriends. If for each integer $k$, any $k$ of the boys have ...


0

As @Trevor Wilson said, $\vdash$ which is named “turnstile” or “right tack”, belongs to the meta‑language, however, it's not always a syntactic consequence operator, it also is a semantic consequence (what @Trevor Wilson said is $\models$), at least in type theory. The model is not only ⊨ , U+22A8, named TRUE in the Unicode database, it's also ⊧ , U+22A7, ...


2

if $B$ is recursive, then you have a recursive function $\chi_B$ such that $\chi_B(x)=1$ iff $x\in B$ else $\chi_B(x)=0$. So from $\chi_B$, and for any set $A$ with $a\in A$ and $z\notin A$, you can compute the function $f$ such that $f(x)=a$ iff $x\in B$ else $f(x)=z$. Using $f$, you can remark that $B\le_m A$. So the sentence is true as long as ...


1

The symbol $\supset$ (called "horseshoe") was used a century ago for the conditional connective "if-then"(see The Notation in Principia Mathematica , and after replaced (mainly) by $\rightarrow$ or $\Rightarrow$. It does not mean that the sentence $A$ is "included" into the sentence $B$. Of course, there is a "relation", through The Algebra of Logic ...


0

Here are some partial answers: A good definition of arrows for $\mathrm{Mod}(T)$ is elementary embeddings of models. It turns out that "being the category of models of a first-order theory" is not a property of a category. Let me explain: let C be the discrete category with an uncountable infinity of objects. Question: is C the category of models of a ...


6

Not sure if this qualifies, but Goodstein's theorem which appears quite number theoretic and states that any Goodstein sequence converges, was proved using ordinals.


1

Hint. To decide $L_1$: Given a word $x$, first decide whether $x \in L_1 \cup L_2$ (using the given decision procedure for the union). If $x$ is not in the union, then $x \not\in L_1$, $x \not\in L_2$. Otherwise enumerate (in parallel) $L_1$ and $L_2$. When $x$ appears (this must happen as $x$ is in the union), then if $x \in L_1$, we are done, if $x \in ...


1

Ps this is just an addition to Peter smiths answer, If you want to upvote this answer then please upvotes peter smiths answr as well. Just to give an correct proof of (iv) 1 | Vx ( Px -> Qx) Premisse . ------------------------------------ 2 | |_____ Ex ( Px & ~Qx) Assumption for ~ Introduction 3 | | |__a Pa & ~Qa ...


3

First we have to "unwid" $(¬A→B)↔¬C$ as : $[(¬A→B)→¬C)]∧[¬C→(¬A→B)]$ and then use the equivalence between : $(¬A→B)$ and $(A∨B)$ and : $(A→B)$ and $(¬A∨B)$. Thus : (i) $(¬A→B)↔¬C$ (ii) $[(¬A→B)→¬C)]∧[¬C→(¬A→B)]$ (iii) $[(A \lor B) \rightarrow \lnot C] \land [\lnot C \rightarrow (A \lor B)]$ (iv) $[\lnot (A \lor B) \lor \lnot C] \land ...


4

So automated theorem provers consist of an application of mathematical logic. Consequently, the solution of the Robbins conjecture by William McCune using EQP qualifies as solving an open problem outside of mathematical logic by using mathematical logic.


11

The Tarski–Seidenberg theorem says that the set of semialgebraic sets is closed under projection. It's a pure real-algebraic statement that was originally proved with logic. Jacobson says this in chapter 5 of his Basic Algebra I: More generally, Tarski's theorem implies his metamathematical principle that any "elementary" sentence of algebra which is ...


10

I was impressed by Bernstein and Robinson's 1966 proof that if some polynomial of an operator on a Hilbert space is compact then the operator has an invariant subspace. This solved a particular instance of invariant subspace problem, one of pure operator theory without any hint of logic. Bernstein and Robinson used hyperfinite-dimensional Hilbert space, a ...


2

(i) to (iii) are indeed not syntactic consequences of the given assumption. (iv) is a syntactic consequence -- but whether your proof is OK will depend on the system you are supposed to be using. In particular, the step from (5) to (6) involves the rule from $\neg\varphi(a)$ infer $\neg\forall x\varphi(x)$ which is certainly sound but it is not usually a ...


-1

i think 1 is true, by applying compactness theorem you can show that 1 is true


2

Tru with a domain $D = \{ a, b \}$ with only two elements, and try to satisfy the formula [you will not succeed ...]. Then try with a domain $D = \{ a_n \}_{n < \omega}$ , with $n$ whatever, and perform the same check : again the answer will be negative. In this way, you will convince ourself that the formula is not satisfiable in a finite domain. ...


1

We have two problems with the formula : $\varphi := \forall x(P(x,y) \rightarrow Q(z,x)) \rightarrow \exists x(\forall yP(x),f(y,z)) \lor \forall z Q(z,x))$ In the formula $\varphi$ we have $7$ left parenthes and $8$ right ones; thus the formula is not well-formed. We have to add a left one, e.g. after the first $\forall x$, or otherwise delete the ...


0

Is this the correct definition of a bounded quantifier? I would say you are talking about "boundable" existential quantifiers, rather than bounded quantifiers. It is true that terms in Peano arithmetic are polynomials, so in the language of Peano arithmetic if we have a bounded quantifier $(\exists x < t(y)) R(x,y)$ then $t(y)$ is a polynomial in ...


3

To add a bit to Mauro ALLEGRANZA 's post about polish notation let $ W_1 = \{N, L, M\} $ and $ W_2 = \{A, C, E, K \} $ and propostional variables are the lower caseletters Then p, Np, Cpq, Kpq, Epq, Apq are all wellformed formulas in polish notation. Also you can replace any propositional variable you with an other propositional variable or with ...


1

Many people define "decidable" for sets $A$ of axioms to mean that the set of theorems provable from those axioms, i.e., the set $C(A)$ of logical consequences of $A$, is computable (= recursive). With this definition, we immediately have that $A$ is decidable if and only if $C(A)$ is decidable, because we always have $C(A)=C(C(A))$. Other people (fewer, I ...


0

In general, a bounded quantifier is the abbreviation of a "standard" first-order formula like : $\forall x (Px \rightarrow Qx)$ which we can abbreviate in slightly different forms according to the contexts : set theory : $\forall x \in P : Qx$, which is : $\forall x(x \in P \rightarrow Qx)$; (formal) arithmetic : $\forall x \le n : Qx$, which is : ...


0

We want to call the above mentoided formula $\varphi(x)$ with $x'$. Therefore, we transform it into an equivalent formula $\varphi'$. $$ \varphi'(x') :=\exists x ( x=x' \land \varphi (x) )$$


2

The definition of : $F : ω → ℘(\mathcal W^{<ω})$ must start for $n = 0$ with all the finite strings starting with a symbol of arity $0$. Buy symbols of arity $0$ are symbols without "argument-places" to be filled. Thus the corresponding expressions will be strings of $lenght = 1$ formed by the symbol itself. I.e. they are the expressions "made of" ...



Top 50 recent answers are included