The propositional logic of here-and-there, denoted by HT, is the superintuitionistic logic characterized by linearly ordered Kripke frames with two worlds (the "here" world and the "there" world). It was introduced by Arend Heyting [Heyting, 1930] as a tool for proving the independence of the law of the excluded middle. Recent interest in HT is related to its role in the theory of logic programming [Lifschitz et al., 2001].

PDF

In Abstracts of Papers Presented at the Third St. Petersburg Days of Logic and Computability 2015.

@inproceedings{harrison:logicdays15, title={A Direct Proof of Hosoi's Theorem (Extended Abstract)}, author={Amelia Harrison and Vladimir Lifschitz and David Pearce and Agustin Valverde}, booktitle={Abstracts of Papers Presented at the Third St. Petersburg Days of Logic and Computability}, url="http://www.cs.utexas.edu/users/ai-labpub-view.php?PubID=127521", year={2015} }