%---- file: QCLAxioms.thf ----------------------------------------------------------------- %--- type mu for individuals; the type \$i is reserved for possible worlds thf(mu,type,(mu:\$tType)). %--- reserved constant for selection function f thf(f,type,(f:\$i>(\$i>\$o)>\$i>\$o)). %--- `exists in world' predicate for varying domains; %--- for each w we get a non-empty subdomain eiw@w thf(eiw,type,(eiw:\$i>mu>\$o)). thf(nonempty,axiom,(![V:\$i]:?[X:mu]:(eiw@V@X))). %--- negation, disjunction, material implic. lifted to possible worlds thf(not,type,(not:(\$i>\$o)>\$i>\$o)). thf(or,type,(or:(\$i>\$o)>(\$i>\$o)>\$i>\$o)). thf(impl,type,(impl:(\$i>\$o)>(\$i>\$o)>\$i>\$o)). thf(not_def,definition,(not = (^[A:\$i>\$o,X:\$i]:~(A@X)))). thf(or_def,definition,(or = (^[A:\$i>\$o,B:\$i>\$o,X:\$i]:((A@X)|(B@X))))). thf(impl_def,definition,(impl = (^[A:\$i>\$o,B:\$i>\$o,X:\$i]:((A@X)=>(B@X))))). %--- conditionality lifted to possible worlds; f is the selection (cf. Stalnaker 1968) thf(cond,type,(cond:(\$i>\$o)>(\$i>\$o)>\$i>\$o)). thf(cond_def,definition,(cond = (^[A:\$i>\$o,B:\$i>\$o,X:\$i]:![W:\$i]:((f@X@A@W)=>(B@W))))). %--- quantification (constant & varying domain, propositional) lifted to possible worlds thf(all_co,type,(all_co: (mu>\$i>\$o)>\$i>\$o)). thf(all_va,type,(all_va:(mu>\$i>\$o)>\$i>\$o)). thf(all,type,(all:((\$i>\$o)>\$i>\$o)>\$i>\$o)). thf(all_co_def,definition,(all_co = (^[A:mu>\$i>\$o,W:\$i]:![X:mu]:(A@X@W)))). thf(all_va_def,definition,(all_va = (^[A:mu>\$i>\$o,W:\$i]:![X:mu]:((eiw@W@X)=>(A@X@W))))). thf(all_def,definition,(all = (^[A:(\$i>\$o)>\$i>\$o,W:\$i]:![P:\$i>\$o]:(A@P@W)))). %--- box operator based on conditionality (illustrates subsumtion of modal logics) thf(box,type,(box:(\$i>\$o)>\$i>\$o)). thf(box_def,definition,(box = (^[A:\$i>\$o]:(cond@(not@A)@A)))). %--- notion of validity of a conditional logic formula (grounding of lifted formulas) thf(vld,type,(vld:(\$i>\$o)>\$o)). thf(vld_def,definition,(vld = (^[A:\$i>\$o]:![S:\$i]:(A@S)))). %---- end file: QCLAxioms.thf -------------------------------------------------------------