@LeakyNun We can't say much. The completeness theorem is non-constructive. Remember that we can't even explicitly describe one countable model of PA that isn't PA itself.
And we can get a non-standard model of PA via the completeness theorem.
There is a theorem that there are no computable non-standard models of PA. This means that there is no computer implementations of the domain and arithmetic operations that obeys PA but is not isomorphic to the standard natural numbers.
Hmm you should learn some computability theory. =)
Nothing to do with lazy evaluation.
We say that a collection of strings is recognizable/decidable/computable iff there is a program that accepts all its members and rejects all other strings.
In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are a set of axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used nearly unchanged in a number of metamathematical investigations, including research into fundamental questions of whether number theory is consistent and complete.
The need to formalize arithmetic was not well appreciated until the work of Hermann Grassmann, who showed in the 1860s that many facts in arithmetic could be derived from more basic facts about...
Oh that's what you mean? You're saying that since one can prove in PA via Godel-coding that there is some sequence of c powers of 2, and can extract that last power, therefore that final power must also be in the domain, which it isn't in our attempt.
I think that's fine, but a rather complicated solution.
> We can have a model $M$ of ZFC, with an inner model $N$ of ZF, such that there is a $\mathbb{Z}/2\mathbb{Z}$-vector space $V\in N$ such that $(i)$ $N\models$"$V$ has no basis" and $(ii)$ $M\models$"$V\cong\bigoplus_{\omega}\mathbb{Z}/2\mathbb{Z}$".
This makes it clearer what inside and outside mean
@LeakyNun Well we can talk in terms of models and inner models, but that means you are talking from a third viewpoint, the 'true' meta-system. Namely, you are in MS considering a model M of ZF that has inside itself a model N of ZF. It is not exactly a minor issue; within ZF we can prove what I said about any countable model of ZF, but within MS you cannot necessarily prove that you even have a model M of ZF in the first place, not to say one that has an inner set model.
Here "y⇒..." says "If y then ..."; that conditional "If y" creates a subcontext, in which you can assert any statement that you have deduced outside that subcontext.
Truth tables are not enough to capture first-order logic (with quantifiers), so we use inference rules instead. Each inference rule is chosen to be sound, meaning that if you start with true statements and use the rule you will deduce only true statements. We say that these rules are truth-preser...
There I describe my variant of Fitch-style ND. You can see immediately what is going on in the logical structure of a proof in this style.
If you look again at the Hilbert-style rules for propositional logic, you will see that they basically capture the notions of reasoning with/under implication.
So everything is very clear from the Fitch-style presentation.
The easiest (and in my opinion cleanest) way to do this is to augment the context. In the sequent calculus you presented, you have the left-hand of the sequent being a set $Γ$ of formulae. Instead of that, you need to have set of sentences $S$ for axioms and a context chain $Q$. $Q$ is an ordered...
The reason I had it in my other system is that it was designed to be as user-friendly as possible, which means friendly for my use because I was the only one using it.
(Until I posted it on Math SE, that is.)
It mirrors how one instantiates variables in modern programming languages.
In practice, I of course use such variable renaming. I did mention a bit about it in that post:
> Renaming quantified variables are unnecessary but would significantly shorten proofs. With renaming rules and omitting the lines in square-brackets the proof is much cleaner yet still easily computer-verifiable:
Under "Example".
So in practice I would write the shorter version using variable-renaming, but technically such rules are superfluous.
Hahaha "natural deduction" is sort of an umbrella term for all such systems. If you're talking about well-known systems, it's true that most of them don't have an explicit rule permitting variable-renaming.
What you would do is to prove that you can use the other rules to perform suitable deductions in order to deduce the same sentence with the variables renamed.
More precisely, you show that every proof that uses variable-renaming rules can be transformed into a proof that doesn't.
In different systems, it's different. In mine, you can use any unused variable name for a new universal context, but you can only use fresh names for existential instantiation.
∃elim: If we prove a ∃-quantified statement, we can use a new variable for a witness for it.
|∃x∈S ( P(x) ).
|...
|------------------------ (where y is a fresh variable)
|Let y∈S such that P(y).
|[y∈S.]
|[P(y).]
It's necessary that y is fresh so that you don't get trouble with y hiding as a bound variable in some previously deduced sentence.
If S:
∃x ( P(x) ).
Let y be such that P(y).
If S:
P(y).
S⇒P(y).
∃x ( S⇒P(x) ).
If ¬S:
Let y be something.
If S:
Contradiction.
P(y).
S⇒P(y).
∃x ( S⇒P(x) ).
∃x ( S⇒P(x) ).
S ⇒ ∃x ( P(x) ).
If ∀x ( ¬(S⇒P(x)) ):
If S:
∃x ( P(x) ).
Let y be such that P(y).
If S:
P(y).
S⇒P(y).
¬(S⇒P(y)).
Contradiction.
¬S.
Let c be something.
If S:
Contradiction.
P(c).
S⇒P(c).
¬(S⇒P(c)).
Contradiction.
¬∀x ( ¬(S⇒P(x)) ).
Yes; they are. The distinction is useful in order to separate classical and intuitionistic logic. With Double Negation or the Law of Excluded Middle, the two version are equivalent; in intuitionistiv logic, where DN and LEM do not hold, RAA does not hold also. — Mauro ALLEGRANZASep 12 at 6:07
@user21820 RAA does not hold in intuitionistic logic?
@LeakyNun Yes. From contradiction you get negation of condition, but you cannot remove negation from condition. It's easy to think using the BHK interpretation, where a proof is literally a program that transforms proofs of premises into a proof of the conclusion. So if you have deduced "( P implies false ) implies false" you literally have a program that transforms a proof of "P implies false" to a proof of "false". Does that give you a program that proves P? Not necessarily.
The following is a classically valid deduction for any propositions $A,B,C$.
$\def\imp{\rightarrow}$
$A \imp B \lor C \vdash ( A \imp B ) \lor ( A \imp C )$.
But I'm quite sure it isn't intuitionistically valid, although I don't know how to prove it, which is my first question.
If my conje...
Using Natural Deduction:
1) $S \to \exists x \ Px$ --- premise
2) $S$ --- assumed [a]
3) $\exists x \ Px$ --- from 1) and 2) by $\to$-elim
4) $Pa$ --- assumed [b] from 3) for $\exists$-elim: $a$ is "fresh", i.e. having no free occurrences in the premise nor in the assumption [a]
5) $S \to Pa...