On First Order Logic of Proofs

2001

50 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computational Theory and Mathematics

View Paper: https://www.semanticscholar.org/paper/3256d9d46164cd6146fbc2bb9598d1063e8b5544

Citations in the corpus

• Explicit provability and constructive semantics (2001, unknown): “c(y) : (∀x A(x)→A(y)) 2(∀x A(x)→A(y)) u :∀x A(x)→(c(y) · u) :A(y) 2∀x A(x)→2A(y) u :∀x A(x)→∀y ((c(y) · u) :A(y)) 2∀x A(x)→∀y 2A(y) In [15] it was shown that the first order logic of proofs is hyperarithmetical (in fact, Π1(TA)-complete, where TA is the set of all true arithmetical sentences).”