section_path: Formal theories/Kripke's semantics
section_name: Kripke's semantics
paragraph_text: Kripke's semantics
  
  Kripke's theory of truth (named after Saul Kripke) contends that a natural language can in fact contain its own truth predicate without giving rise to contradiction. He showed how to construct one as follows:
  
  Truth never gets defined for sentences like This sentence is false, since it was not in the original subset and does not predicate truth of any sentence in the original or any subsequent set. In Kripke's terms, these are "ungrounded." Since these sentences are never assigned either truth or falsehood even if the process is carried out infinitely, Kripke's theory implies that some sentences are neither true nor false. This contradicts the principle of bivalence: every sentence must be either true or false. Since this principle is a key premise in deriving the liar paradox, the paradox is dissolved.
  
  The proof sketch for Gödel's first incompleteness theorem shows self-reference cannot be avoided naively, since propositions about seemingly unrelated objects can have an informal self-referential meaning; in Gödel's work, these objects are integer numbers, and they have an informal meaning regarding propositions. In fact, this idea — manifested by the diagonal lemma —is the basis for Tarski's theorem that truth cannot be consistently defined.
  
  It has thus been claimed that Kripke's system indeed leads to contradiction: while its truth predicate is only partial, it does give truth value (true/false) to propositions such as the one built in Tarski's proof, and is therefore inconsistent. While there is still a debate on whether Tarski's proof can be implemented to every similar partial truth system, none have been shown to be consistent by acceptable methods used in mathematical logic.
  
  Kripke's semantics are related to the use of topoi and other concepts from category theory in the study of mathematical logic. They provide a choice of formal semantics for intuitionistic logic.