User Lucas K.

13 votes

3 answers

1k views

Reducing ACA₀ proof to First Order PA

asked May 6, 2010 at 21:39

13 votes

4 answers

4k views

Is finitism an extreme form of constructivism?

asked Jan 10, 2011 at 20:57

9 votes

1 answer

634 views

Starting Hilbert's Program on the other end

asked Mar 2, 2014 at 21:01

5 votes

1 answer

666 views

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

asked Aug 22, 2015 at 22:17

5 votes

3 answers

2k views

Can the omega-rule rescue Hilbert's program?

asked Jan 9, 2016 at 23:35

5 votes

2 answers

342 views

Can a universal induction rule be formulated?

asked Nov 27, 2016 at 22:30

5 votes

2 answers

963 views

Program transformation as alternative for Hoare logic or temporal logic

asked Jul 9, 2011 at 22:27

4 votes

2 answers

279 views

Is there any literature about inner-replacement rule?

asked Dec 29, 2011 at 23:53

4 votes

0 answers

268 views

Primitive Closure Arithmetic

asked Jun 7, 2015 at 22:23

3 votes

2 answers

1k views

Propositional logic without negation

asked Jul 13, 2015 at 22:27

3 votes

1 answer

408 views

Reference request, proof about well-ordering of ordinals

asked Mar 20, 2016 at 22:02

3 votes

2 answers

452 views

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

asked Mar 26, 2012 at 21:59

3 votes

1 answer

146 views

Defining functions in FOL + PA

asked Sep 5, 2022 at 22:10

2 votes

3 answers

659 views

logics restricted in arithmetic hierarchy

asked Nov 23, 2010 at 21:42

2 votes

4 answers

1k views

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

asked Aug 11, 2010 at 18:21

1 vote

1 answer

514 views

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

asked Oct 28, 2010 at 19:54

1 vote

2 answers

1k views

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

asked May 20, 2010 at 21:43

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?

asked Apr 8, 2012 at 18:25

1 vote

2 answers

435 views

Are Separation and Types the only way to avoid paradoxes?

asked Jan 2, 2017 at 20:32

1 vote

0 answers

513 views

Single logic foundation vs. multi-logic foundation

asked Jan 24, 2011 at 20:43

0 votes

1 answer

156 views

How to ensure a clean conservative extension in general?

asked May 1, 2017 at 21:22

Stack Exchange Network

21 Questions

Reducing ACA₀ proof to First Order PA

Is finitism an extreme form of constructivism?

Starting Hilbert's Program on the other end

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

Can the omega-rule rescue Hilbert's program?

Can a universal induction rule be formulated?

Program transformation as alternative for Hoare logic or temporal logic

Is there any literature about inner-replacement rule?

Primitive Closure Arithmetic

Propositional logic without negation

Reference request, proof about well-ordering of ordinals

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

Defining functions in FOL + PA

logics restricted in arithmetic hierarchy

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

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

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

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?

Are Separation and Types the only way to avoid paradoxes?

Single logic foundation vs. multi-logic foundation

How to ensure a clean conservative extension in general?