Lucas K.'s user avatar
Lucas K.'s user avatar
Lucas K.'s user avatar
Lucas K.
  • Member for 13 years, 10 months
  • Last seen more than a week ago
  • The Netherlands
13 votes
3 answers
1k views

Reducing ACA₀ proof to First Order PA

13 votes
4 answers
3k views

Is finitism an extreme form of constructivism?

9 votes
1 answer
620 views

Starting Hilbert's Program on the other end

6 votes
2 answers
899 views

Program transformation as alternative for Hoare logic or temporal logic

5 votes
1 answer
587 views

What are key $\Sigma^0_2$ or $\Pi^0_3$ theorems?

5 votes
3 answers
2k views

Can the omega-rule rescue Hilbert's program?

5 votes
2 answers
329 views

Can a universal induction rule be formulated?

4 votes
0 answers
265 views

Primitive Closure Arithmetic

4 votes
2 answers
278 views

Is there any literature about inner-replacement rule?

3 votes
2 answers
1k views

Propositional logic without negation

3 votes
1 answer
361 views

Reference request, proof about well-ordering of ordinals

3 votes
1 answer
145 views

Defining functions in FOL + PA

2 votes
3 answers
622 views

logics restricted in arithmetic hierarchy

2 votes
2 answers
429 views

How do you restrict the induction axiom in second (or higher) order logic?

2 votes
4 answers
1k views

Can transfinite induction be defined as axiom scheme in FOL on bin-tree structures?

1 vote
1 answer
510 views

Can invariant of transitive reflexive closure in FOL+PA always been proven?

1 vote
2 answers
1k views

Can Goodstein's theorem been proven with first order PA + Constructive Omega Rule?

1 vote
2 answers
1k views

Is there a natural example of a second order proof that does not reduce to a first order proof in a straight forward way, if all variables are filled in?

1 vote
2 answers
417 views

Are Separation and Types the only way to avoid paradoxes?

1 vote
0 answers
507 views

Single logic foundation vs. multi-logic foundation

0 votes
1 answer
154 views

How to ensure a clean conservative extension in general?