Editing Three-valued logic (section)

=== HT logic ===
{{further|Intermediate logic}}
{{further|Many-valued logic#Gödel logics Gk and G∞}}
The logic of here and there ('''HT''', also referred as Smetanov logic '''SmT''' or as [[Gödel]] G3 logic), introduced by [[Heyting]] in 1930<ref>{{cite journal |last1=Heyting |title=Die formalen Regeln der intuitionistischen Logik. |journal=Sitz. Berlin |date=1930 |volume=42–56}}</ref> as a model for studying [[intuitionistic logic]], is a three-valued [[intermediate logic]] where the third truth value NF (not false) has the semantics of a proposition that can be intuitionistically proven to not be false, but does not have an intuitionistic proof of correctness.

{| style="border-spacing: 10px 0;" align="center"
| colspan="3" style="text-align:center;" | (F, false; NF, not false; T, true)
|- valign="bottom"
|
{| class="wikitable" style="text-align:center;"
|+ NOT{{sub|HT}}(A)
! width="25" | A
! width="25" | ¬A
|-
! scope="row" {{no|F}}
| {{yes|T}}
|-
! scope="row" | NF
| {{no|F}}
|-
! scope="row" {{yes|T}}
| {{no|F}}
|}
|}
{| style="border-spacing: 10px 0;" align="center"
|- valign="bottom"
|
{| class="wikitable" style="text-align:center;"
|+ IMP{{sub|HT}}(A, B)
! rowspan="2" colspan="2" | A → B
! colspan="3" |B
|-
! width="25" {{no|F}}
! width="25" | NF
! width="25" {{yes|T}}
|-
! rowspan="3" |A
! scope="row" {{no|F}}
| {{yes|T}}
| {{yes|T}}
| {{yes|T}}
|-
! scope="row" | NF
| {{no|F}}
| {{yes|T}}
| {{yes|T}}
|-
! scope="row" width="25" {{yes|T}}
| {{no|F}}
| NF
| {{yes|T}}
|}
|}

It may be defined either by appending one of the two equivalent axioms {{nowrap|(¬''q'' → ''p'') → (((''p'' → ''q'') → ''p'') → ''p'')}} or equivalently {{nowrap|''p''∨(¬''q'')∨(''p'' → ''q'')}} to the axioms of [[intuitionistic logic]], or by explicit truth tables for its operations. In particular, conjunction and disjunction are the same as for Kleene's and Łukasiewicz's logic, while the negation is different.

HT logic is the unique [[atom (order theory)|coatom]] in the lattice of intermediate logics. In this sense it may be viewed as the "second strongest" intermediate logic after classical logic.