bio  website  

location  
age  
visits  member for  4 years, 5 months 
seen  Jun 2 '11 at 9:03  
stats  profile views  45 
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 cutfree 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 noncomprehension 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 cutfree 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 typechecking would be undecidable. In order to check whether $(S,*)$ has type semigroup, the typechecker 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 FirstOrder Arithmetic", they give the modeltheoretic 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 