On The Logic Of Justification

The logic of justification is logic systems for reasoning about epistemic justification. Regarding justification operator which is missing in the process of traditional logic formalizing as its subject, the logic of justification absorbs mainstream mathematical theory of proof and epistemology ideas, and is established on classical propositional logic.The logic of proof is the first member of the family of the justification logic. Its history can be traced back to Godel’s thought of construing □F as Provable(F), and makes it equivalent to (?) xProof(x, F), Artemov interprets □F as relation function Proof(t,F). He thinks the conversion from implicit term to explicit term not only realizes S4 properly embedding in LP, reasonably avoids its violation of Godel’s second incompleteness theorem, but also provides a long-anticipated exact provability semantics for provability logic S4. Later, Artemov applies the logic of proof to epistemology, and develops a family of justification systems.But Artemov doesn’t treat the logic of proof as the basic system of Justification logic. He takes the logic system J which only has the application axiom and sum axiom as the standard system. In system J, t:F doesn’t read that t is a proof of F, but rather t is a justification of F. t is proof polynomials which is built from justification variables and justification constants by means of the unitary operator proof checker’!’and binary operators application’·’、sum’+’. When t is the justification constant, F is the axiom of J, the set of all formulae of t:F is called the constant specifications. The derivations in justification logic carry out with the given constant specifications, because they specify the justification terms of axioms, fundamentally show the justification basis of J. The semantic model of J is Kripke model with admissible evidence function ε(t, F), the former is the mapping from justification polynomial and the set of formulae to the possible world. Respect to Kripke semantic model, J is sound and completeness. By adding the axioms from logical awareness、 adequacy、positive inspection、negative introspection rules to J, the result of other justification systems J4、J45、JT、JT4、JT45 and JD45 are also sound and completeness.Due to transforming □F to t:F, the logic of justification gets rid of the Logical Omniscience defect of the modal logic of knowledge, which makes us more securely expand our konwledge. In the aspect of describing common knowledge, justification logic makes us aware of the reasons behind the knowledge, the cut-elimination rule it has makes the process of getting common knowledge reasonable and possible, which make up the defect of traditional cognition logic in theory and practice. Yet the describing of the firse-order justification logic to the Gettier’s problems, not only reveals their essence, but also shows justification logic’s powerful expression ability.Justification logic is the newly developing subject of epistemic logic and it has large space for development, such as quantified justification logic、the construct of systems of S4LP、LPP. Thus the study of it has important subject and age significance. Base on the understanding of relative classical papers, this paper systemically hackles the development of justification, illustrates its content in detail, properly evaluates its value in philosophy and application.