The notion of formal proof is defined by finite sequences ($<\omega$ - sequences) of sentences. In some sense if a sentence $\sigma$ is (finitely) provable from the theory $T$ it is very "near" to ...
I am puzzling with the question which of the two proof systems (Hilbert style axiomatic proofs or substructural Sequent Calculi) is the most discriminatory? With discriminatory I mean is which proof ...
In Gentzen's sequent calculus, a formal proof is described by a tree, with each node representing the sequent obtained from the child(ren) by applying a given inference rule. If no inference rule has ...
Technically, it is possible to prove anything in Coq proof assistant  (on at least Linux) due to a programming feature (or bug). This seems tractable when validating large proofs. Human analysis ...