[FOM] Cut elimination for second order logic

[Aatu Koskensilta]

  Cut elimination for second-order logic implies the consistency of second-order arithmetic, as is well-known, so one would expect to find in your paper some indication of where the argument invokes this or that principle, or relies in this or that notion, that goes beyond second-order arithmetic. Presumably this is also what the referees were asking about. It would probably be a good idea to explicitly address this concern, if only to reassure potential readers that working through your proof, which I haven't studied in any detail myself, is not just an exercise in error spotting.

  Best,
Aatu Koskensilta (koskensilta.aatu.j at student.uta.fi)

"Wovon man nicht sprechen kann, darüber muss man schweigen"
 - Ludwig Wittgenstein, Tractatus Logico-Philosophicus



-- 
Aatu Koskensilta (koskensilta.aatu.j at student.uta.fi)

"Wovon man nicht sprechen kann, darüber muss man schweigen"
 - Ludwig Wittgenstein, Tractatus Logico-Philosophicus
> On 07 Jun 2016, at 10:41, Sandro Skansi <skansi.sandro at gmail.com> wrote:
> 
> Dear FOMers,
> 
> After trying to publish my paper on with a constructive proof for cut elimination for second order logic for three years and never getting past the editors whose response was basically a politer version of "I think this should not be provable, pass", I decided to give up. I understand that the top priority for journal editors is to ensure a high precision since this, and not recall is how they get evaluated, so I decided to publish my paper on arXiv
> 
> https://arxiv.org/abs/1606.01763
> 
> I also made a Python program which implements the algorithm correctly, and in my view (based on the idea that computable functions are a subset of all functions), a program that runs the algorithm is a proof stronger than any mathematical proof resting on indirect constructions such as EFQ. What are your opinions on the subject of editor discretion and program-as-proof (not just in the Curry-Howard sense, but in the sense of a stronger proof than a humanly checkable proof by contradiction)
> 
> Cheers,
> Sandro
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160611/ab737dbf/attachment.html>