[isabelle] Formalization of "The logic of negationless mathematics"

[anderso...@gmail.com]

Hi.

I'm trying to formalize in Isabelle Vredenduin's logic of negationless mathematics (1953). As usual, my code starts with:

"typedecl o
typedecl i

judgment
Trueprop :: "o ⇒ prop" ("_" 5)


subsection {* Propositional logic *}

axiomatization
imp :: "o ⇒ o ⇒ o" (infixr "→" 25) and
conj :: "o ⇒ o ⇒ o" (infixr "∧" 35) and
disj :: "o ⇒ o ⇒ o" (infixr "∨" 35) and
Ex :: "(i ⇒ o) ⇒ o" (binder "∃" 10) and
All :: "(i ⇒ o) ⇒ o" (binder "∀" 10)"

However, in Vredenduin's work, there are no type distinction between propositions and propositional functions. Thus, p → q may be both of type "o ⇒ o ⇒ o" and of type "_=>_ ⇒ _=>_ ⇒ _=>_". How could I deal with this issue? And what about the case of quantifiers?