176 reputation
2
bio website
location
age
visits member for 4 years, 1 month
seen Jun 2 '11 at 9:03

May
27
comment Reducing ACA₀ proof to First Order PA
Actually, what I wrote way back last July is not quite correct, since free set variables might occur in the induction axioms used in $ACA_0$. But it's reparable. $\Delta$ is a cut-free proof of $\Gamma, \forall x_1(x_1 \in X_1 \leftrightarrow \phi_1), \ldots, \forall x_n (x_n \in X_n \leftrightarrow \phi_n) \vdash \alpha$, where $\Gamma$ is some finite sequence of the non-comprehension axioms of $ACA_0$. Replace $t \in X_i$ with $[t/x_i]\phi_i$, and $t \in Y$ with $t = t$ for every other set variable $Y$.
May
27
comment Reducing ACA₀ proof to First Order PA
I meant $\Delta$ to be a cut-free proof in pure predicate logic (LK) of a sequent of the form $\Gamma, \forall x_1(x_1 \in X_1 \leftrightarrow \phi_1), \ldots, \forall x_n (x_n \in X_n \leftrightarrow \phi_n) \vdash \alpha$, where \Gamma is some finite sequence of axioms of PA.
Jan
29
answered What is the intuitive meaning of star and box in a pure type system?
Jan
29
comment Is P=NP relevant to finding proofs of everyday mathematical propositions?
Very pedantic point: I think you mean $T \vdash \phi$ or $T \vdash \neg \phi$' under 1, not $T \vdash \phi \vee \neg \phi$', which is true for all $\phi$ (if we're using classical logic).
Jul
28
comment What is a semigroup or, what do I do with that associativity proof?
I'm late to the party, I know, but: Coq keeps the proof object because otherwise type-checking would be undecidable. In order to check whether $(S,*)$ has type semigroup, the type-checker would need to decide whether there exists a proof of $\forall x,y,z : S. (x*y)*z = x*(y*z)$, and this is undecidable in general.
Jul
21
comment Is reflexivity of equality an axiom or a theorem?
There's one property that cannot be proved from this definition: $2) x = y \wedge x \in z \rightarrow y \in z$ If we take $x=y$ to be an abbreviation for 1), then we must add 2) as an axiom.
Jul
20
awarded  Supporter
Jul
19
answered Most general formulation of Gödel's incompleteness theorems
Jul
5
comment Reducing ACA₀ proof to First Order PA
More: In Petr Hájek and Pavel Pudlák's book "Metamathematics of First-Order Arithmetic", they give the model-theoretic proof (Theorem III.1.16) and show that it is formalisable in $I \Sigma_1$, the subtheory of PA in which induction is restricted to $\Sigma_1$-formulas (Theorem IV.4.10).
Jul
1
awarded  Teacher
Jul
1
answered Reducing ACA₀ proof to First Order PA