IntroductionValidityLocal Soundness and CompletenessSample ProofsProof TermsA CounterexampleLecture Notes onCategorical Judgments15-816: Modal LogicFrank PfenningLecture 3January 19, 20101 IntroductionThe main basic judgments we have considered so far are:A true A is trueA↑ A has a verificationA↓ A may be usedM : A M is a proof term for A, or, equivalently,M has type AIn addition, we have considered hypothetical judgments J1, . . . , Jn` J ingeneral, and x1:A1, . . . , xn:An` M : C in particular.A few crucial properties of these systems are still outstanding. In partic-ular, we still need to prove global versions of the local soundness and com-pleteness properties. We call them here internal soundess and completenessto remind us that they refer to properties of proofs and verifications, ratherthan to any external semantics in terms of mathematical structures.Internal Soundness. If A↑ and A↓ ` C↑ then C↑.Internal soundness licenses us to use A in verifications of C, if we havea verification of A. This means that, globally, the elimination rules are nottoo strong: we cannot abuse the assumption A to deduce something thatdoes not have a verification already.Internal Completeness. A↓ ` A↑.LECTURE NOTES JANUARY 19, 2010L3.2 Categorical JudgmentsInternal completeness show that the elimination rules are strong enoughso that we can construct a verification of A, if given the license to use A.In addition, we would like to relate verifications to the notion of truth,viewing (as verificationists like myself tend to do) uses as an auxiliary judg-ment form.Truth and Verifications. A true if and only if A↑.The proof that A is true exactly if it has a verification is rather straight-forward, once we have established internal soundness and completeness.We will return to these properties in a later lecture. In this lecture wepresent a generic and frequent construction of a new kind of judgment froma given one, by insisting that it be proved without using assumptions. Thepresentation in this lecture is based closely on [PD01].2 ValidityWe say that A is valid if A true has a proof that does not require any truthassumptions. The latter is an example of a categorical judgment, a judgmentwhich does not depend on assumptions. We write • ` A true for a categor-ical judgment, emphasizing that there are no truth hypotheses. Formally,‘•’ is synonymous with ‘·’, our prior notation for an empty collection ofhypotheses.Definition of Validity. A valid if • ` A true.Now we would like to ask questions such as: If A ⊃ B and A are bothvalid, is B also valid? In order to be able to ask the question we wouldlike to reflect the notion of validity as a proposition. This proposition istraditionally written as A. A first introduction rule for this could simplybeA validΓ ` A true I1Note that we lose the assumptions Γ, since a proof of validity is not permit-ted to depend on truth assumptions, which are collected in Γ.It turns out to be convenient for the judgment A valid never to appearas the conclusion of a hypothetical judgment. In order to achieve this, wejust replace it with its definition.• ` A trueΓ ` A true I2LECTURE NOTES JANUARY 19, 2010Categorical Judgments L3.3As an introduction rule, this is rather straightforward. In our judgmen-tal formulation, the complexity of A comes from the elimination rule.A first attempt would be to simply reverse the introduction rule.Γ ` A true• ` A true E1?This would seem to be locally sounds, but it misinterprets the notion ofhypothetical judgment. Clearly, we use Γ to deduce A; dropping this listof assumptions is not justified. For example, A true ` A truehyp• ` A true E1?would mean that we can derive an arbitrary proposition from no assump-tion, which renders the system meaningless. The rule above is unsound.Another attempt would be to simply extract A true.Γ ` A trueΓ ` A true E2?This is clearly locally sound, but is not locally complete:DΓ ` A true=⇒EDΓ ` A trueΓ ` A true E2?Γ ` A true I??The problem is of course that the introduction rule does not apply becausethe hypotheses are not empty.The solution is to introduce A valid as a new form of hypothesis. Thejudgment we consider then has the general formu1::B1valid, . . . , uk::Bkvalid| {z }∆; x1:A1true, . . . , xn:Antrue| {z }Γ` C trueAs usual, we assume all the ujand xiare distinct and maintain this invari-ant through renaming of bound variables as needed.The elimination form now just makes the validity of A available as anassumption.∆; Γ ` A true (∆, u::A valid); Γ ` C true∆; Γ ` C true EuLECTURE NOTES JANUARY 19, 2010L3.4 Categorical JudgmentsWe also have to reexamine the introduction rule, now that we have addi-tional hypotheses. The idea is that the assumptions in ∆ are valid, andshould therefore be available in the proof of A valid, while the truth as-sumptions in Γ must be erased. In short:∆; • ` A true∆; Γ ` A true IOf course, there also must be some way to actually use hypothesesA valid. The nature of hypothetical judgments yields (∆, A valid); Γ ` A valid,except that A valid is not a permissable conclusion. So instead we infer thatA is true, which is correct by the definition of validity.u::A valid ∈ ∆∆; Γ ` A trueuAll other rules of natural deduction are extended systematically, fol-lowing the nature of hypothetical judgments. This kind of extension iscompletely implicit in the usual two-dimensional form of natural deduc-tion, which is inherently open-ended as to what kind of other hypothesesmight be needed to explain new propositions. In the localized form, whichis convenient for the analysis of the rules, we just add valid hypotheses ∆to the premises and conclusions of all rules.3 Local Soundness and CompletenessWith a new form of hypothesis, we obtain a new substitution principle.Substitution Principle for Validity, v.1: If ∆ ` A valid and(∆, u::A valid); Γ ` C true then ∆; Γ ` C true.However, we decided to use validity only in assumptions and never ex-plicitly as a conclusion, so we replace the first assumption by its definition.Substitution Principle for Validity, v.2: If ∆; • ` A true and(∆, u::A valid); Γ ` C true then ∆; Γ ` C true.Note that it is crucial that there are no truth assumptions in the proof ofA true; otherwise A would not be valid!LECTURE NOTES JANUARY 19, 2010Categorical Judgments L3.5Now local soundness is easy to check.D∆; • ` A true∆; Γ ` A true IE(∆, u::A