[FOM] Cut elimination for second order logic

[Sandro Skansi]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160607/ef17e495/attachment.html>