#
# == Notation for truth ==
#
# Although ghilbert can, basically, define truth and falsity in terms of prop.ghi, it doesn't appear to have the ability to give a notation for truth (⊤) or falsity (⊥) without an additional axiom. We adopt an axiom that asserts that ⊤ holds, which is enough (⊥ can be defined in terms of ⊤).
param (PROP ../peano/prop.ghi () "")
term (wff (⊤))
stmt (True () () (⊤))