@Tung In what context? You can define it to be the total # of symbols or the total # of purely logical symbols or the # of atomic formula. Really depends on what your goal is
@TungNguyen There are many different ways of defining length of a formula in first-order logic that would work for the desired purposes. The reason is that the underlying idea is structural induction (as David described). Now I think you should actually look at the rigorous form of structural induction itself.
For CS students specifically, there is another approach that would work better than the usual way induction is taught, namely by teaching structural induction, which goes like this:
If you want to prove that a collection $S$ of finite structures (such as binary trees) satisfy a property $P$, ...
It applies whenever you have a collection S and a function f : S → N, and a predicate P : S → bool. Then structural induction says: ∀x∈S ( ∀y∈S ( f(y)<f(x) ⇒ P(y) ) ⇒ P(x) ) ⇒ ∀x∈S ( P(x) ).
Otherwise condition (2) suffices. Namely, if you can show that ( given any object x in S, if every object in S of smaller size than x satisfies P, then x itself satisfies P ), then every object in S satisfies P. Size is captured above by f.
Incidentally, you can prove structural induction by using classical logic plus ordinary induction alone. I always recommend my students to try this haha..
@DavidReed If you're referring to the topic of evidence for first-order logic that you raise in the other room, feel free to continue here. It's just that it would be a different discussion since over there it's about whether the post is bad or not rather than about the non-mathematical philosophical issues.
@DavidReed I'm not sure how to interpret that question. I'm fine, as usual.
@user21820 enumerate all 1-parameter sentences P such that ${\sf ZFC} \vdash \exists!x P(x)$ as $P_n(x)$. Now, let $X = \{n \in \Bbb N \mid {\sf ZFC} \vdash \forall x (P_n(x) \to x \notin \mathcal P(\Bbb N))\}$. Now is it true that $X \in \mathcal P(\Bbb N)$?
@LeakyNun Well by power-set axiom of course X ⊆ N.
@LeakyNun I knew you'd want to do that. If you're lazy, you can take the lazy approach to intuitively understand what goes wrong. You wish to work inside ZFC itself. ZFC could be consistent but proves itself inconsistent. So you would be enumerating all 1-parameter sentences over ZFC, and also your X would be just the collection of all natural numbers.
@LeakyNun My point is only that the lazy approach shows that whatever argument you have in mind is bound to fail because ZFC can't prove the scenario above doesn't happen.
Assume $k \in X$, so ${\sf ZFC} \vdash X \notin \mathcal P(\Bbb N)$, which is absurd. Assume $k \notin X$, so ${\sf ZFC} \nvdash X \notin \mathcal P(\Bbb N)$, so $k \in X$.
Though your previous attempt failed, I'm quite sure you can obtain some undefinability result if you carefully extract the required assumption needed to push your argument through.
Enumerate all 1-parameter sentences P such that ${\sf ZFC} \vdash \exists!x P(x)$ as $P_n(x)$. Now, let $X = \{n \in \Bbb N \mid \mathcal M \vDash \forall x (P_n(x) \to x \notin \mathcal P(\Bbb N))\}$ where $\mathcal M$ is a model of ZFC.
Assume $k \in X$, so ${\cal M} \vDash X \notin \mathcal P(\Bbb N)$, which is absurd. Assume $k \notin X$, so ${\sf M} \nvDash X \notin \mathcal P(\Bbb N)$, so $k \in X$.
So what? If your claim does not type-check, then you cannot make it. You would need some type-conversion mapping, and such simply does not exist.
That's why I said you should observe carefully how I define definable reals, because I'm avoiding this exact same problem by considering only models with the same reals.
Let us be more precise about definable numbers, to avoid common pitfalls.
Suppose we have chosen our favourite foundational system $S$, which is in modern mathematics ZFC. $S$ of course can be implemented by a computer program that will given any input theorem and purported proof will output "ye...
I'm not quite getting your informal type-check... M is a model of ZFC but by definition of model M could be anything; it's unrelated to the current world in which you're reasoning.
I think I get the same obstruction. Though obj is the universe, I cannot prove that it is a model of the system, and so we cannot talk about what it satisfies.
So perhaps you can indeed say that your issue is with assuming the existence of a model that is an isomorphic copy of the universe itself.
Sanity check, does $\sf PA$ (the usual $6$ axioms plus the first order induction schema) prove that there is no $x$ with $0<x<S(0)$? (where the order relation is defined as $x<y\iff\exists z(z\neq 0\land x+z=y)$?
Or better, does $\sf PA$ prove $\forall x(x\neq 0\rightarrow \exists y(x=S(y)))$? What about $\sf PA^2$ defined as the usual $6$ axioms plus the second order induction axiom "every nonempty subset has a minimum"?
@AlessandroCodenotti re $0<x<S(0)$: Let $0+S(m)=x$ and $x+S(n)=S(0)$, where $S(m)$ and $S(n)$ are guaranteed by lemma. Substitution gives $S(m)+S(n)=S(0)$, whence $S(S(m)+n)=S(0)$, whence $S(m)+n=0$, whence $S(m+n)=0$ (through induction), whence contradiction
Another question, let $L=\{+,-,\cdot,0,1,<\}$ be the language of ordered fields, we consider the L-structure $\Bbb R$ (where everything has the obvious interpretation) and the theory of that structure $\text{Th}(\Bbb R)$. By Löwenheim-Skolem there is a countable model of $\text{Th}(\Bbb R)$ (which is also elementarily equivalent to $\Bbb R$), what does such a model look like? I suspect the algebraic numbers might work but I'm not sure
Yes.
The reason is that the two fields are models of the complete theory of Real-Closed Fields. One of the characterization of real-closed fields is that their algebraic closure is an extension of degree $2$, which is clearly true for both fields.
Beware that you need the real algebraic numbers
> Examples of real closed fields[edit] the real algebraic numbers the computable numbers the definable numbers the real numbers superreal numbers hyperreal numbers the Puiseux series with real coefficients
Ok, one more sanity check, any two models of $\sf PA$ contain an isomorphic initial segment, any two models of $\sf PA^2$ are isomorphic
Given two models $A$ and $B$ and the function $f(0_A)=0_B$ and $f(S_A(x))=S_B(f(x))$ it can be proved that this is an isomorphism if $A$ and $B$ model $\sf PA^2$ but just an injective homeomorphism if they model $\sf PA$, right?
Yes.
The reason is that the two fields are models of the complete theory of Real-Closed Fields. One of the characterization of real-closed fields is that their algebraic closure is an extension of degree $2$, which is clearly true for both fields.
