H

Idea

$\mathtt{H}$ is a standard classical higher-order logic used as background logic for the formulations of various systems of higher-order logic of philosophical interest, such as Classicism.

Axiomatization

Axiom instances include both open and closed terms. $\Phi [A]$ stands for a term with an occurrence of $A$, and $\Phi [B]$ stands for the result of replacing that very occurrence of $A$ with $B$. Free variables in $A$ are allowed.

• $⊢P$ when $P$ is a classical tautology (Taut)
• $⊢\forall F\to FA$ (UI)
• $⊢FA\to \exists F$ (EG)
• $⊢A=A$ (Ref)
• $⊢A=B\to FA=FB$ (LL)
• $⊢\Phi [(\lambda v.A)B]\leftrightarrow \Phi [A[v/A]]$ when $v$ is substitutable for $A$ ($\beta$)
• $⊢\Phi [\lambda v.Fv]\leftrightarrow \Phi [F]$ when $v$ is not free in $F$ ($\eta$)
• If $⊢P$ and $⊢P\to Q$ then $⊢Q$ (MP)
• If $⊢P\to Q$ and $v$ is not free in $P$ then $⊢P\to \forall vQ$ (Gen)
• If $⊢P\to Q$ and $v$ is not free in $Q$ then $⊢\exists vP\to Q$ (Inst)