An arithmetic interpretation of intuitionistic verification

2020 ◽  
Vol 30 (1) ◽  
pp. 381-402
Author(s):  
Tudor Protopopescu
Keyword(s):  
Intuitionistic Logic ◽  
Epistemic Logic ◽  
Logic Of Proofs ◽  
Precise Formulation ◽  
Fundamental Assumption ◽  
Bhk Semantics

Abstract Intuitionistic epistemic logic introduces an epistemic operator to intuitionistic logic, which reflects the intended Brouwer–Heyting–Kolmogorov (BHK) semantics of intuitionism. The fundamental assumption concerning intuitionistic knowledge and belief is that it is the product of verification. The BHK interpretation of intuitionistic logic has a precise formulation in the logic of proofs and its arithmetical semantics. We show here that this interpretation can be extended to the notion of verification upon which intuitionistic knowledge is based, providing the systems of intuitionistic epistemic logic based on verification with an arithmetical semantics too. This confirms that the conception of verification incorporated in these systems reflects the BHK interpretation.

scholarly journals Co-constructive Logics for Proofs and Refutations

Studia Humana ◽  
2015 ◽  
Vol 3 (4) ◽  
pp. 22-40 ◽  
Author(s):  
James Trafford
Keyword(s):  
Intuitionistic Logic ◽  
Proof Theory ◽  
Direct Proof ◽  
Negative Information ◽  
Constructive Logic ◽  
Logic Of Proofs ◽  
Constructive Logics

Abstract This paper considers logics which are formally dual to intuitionistic logic in order to investigate a co-constructive logic for proofs and refutations. This is philosophically motivated by a set of problems regarding the nature of constructive truth, and its relation to falsity. It is well known both that intuitionism can not deal constructively with negative information, and that defining falsity by means of intuitionistic negation leads, under widely-held assumptions, to a justification of bivalence. For example, we do not want to equate falsity with the non-existence of a proof since this would render a statement such as “pi is transcendental” false prior to 1882. In addition, the intuitionist account of negation as shorthand for the derivation of absurdity is inadequate, particularly outside of purely mathematical contexts. To deal with these issues, I investigate the dual of intuitionistic logic, co-intuitionistic logic, as a logic of refutation, alongside intuitionistic logic of proofs. Direct proof and refutation are dual to each other, and are constructive, whilst there also exist syntactic, weak, negations within both logics. In this respect, the logic of refutation is weakly paraconsistent in the sense that it allows for statements for which, neither they, nor their negation, are refuted. I provide a proof theory for the co-constructive logic, a formal dualizing map between the logics, and a Kripke-style semantics. This is given an intuitive philosophical rendering in a re-interpretation of Kolmogorov's logic of problems.

Epistemic logic: All knowledge is based on our experience, and epistemic logic is the cognitive representation of our experiential confrontation in reality

Semiotica ◽  
2020 ◽  
Vol 0 (0) ◽  
Author(s):  
Dan Nesher
Keyword(s):  
Intuitionistic Logic ◽  
Epistemic Logic ◽  
Basic Science ◽  
Formal Semantics ◽  
Self Control ◽  
Cognitive Representation ◽  
Metaphysical Realism ◽  
True Representation ◽  
Excluded Middle

AbstractEpistemic Logic is our basic universal science, the method of our cognitive confrontation in reality to prove the truth of our basic cognitions and theories. Hence, by proving their true representation of reality we can self-control ourselves in it, and thus refuting the Berkeleyian solipsism and Kantian a priorism. The conception of epistemic logic is that only by proving our true representation of reality we achieve our knowledge of it, and thus we can prove our cognitions to be either true or rather false, and otherwise they are doubtful. Therefore, truth cannot be separated from being proved and we cannot hold anymore the principle of excluded middle, as it is with formal semantics of metaphysical realism. In distinction, the intuitionistic logic is based on subjective intellectual feeling of correctness in constructing proofs, and thus it is epistemologically encapsulated in the metaphysical subject. However, epistemic logic is our basic science which enable us to prove the truth of our cognitions, including the epistemic logic itself.

scholarly journals The basic intuitionistic logic of proofs

2007 ◽  
Vol 72 (2) ◽  
pp. 439-451 ◽  
Author(s):  
Sergei Artemov ◽  
Rosalie Iemhoff
Keyword(s):  
Intuitionistic Logic ◽  
Basic Logic ◽  
Logic Of Proofs ◽  
Complete Axiomatization ◽  
Heyting Arithmetic ◽  
Propositional Language

AbstractThe language of the basic logic of proofs extends the usual propositional language by forming sentences of the sort x is a proof of F for any sentence F. In this paper a complete axiomatization for the basic logic of proofs in Heyting Arithmetic HA was found.

scholarly journals An Analytic Calculus for the Intuitionistic Logic of Proofs

2019 ◽  
Vol 60 (3) ◽  
pp. 353-393
Author(s):  
Brian Hill ◽  
Francesca Poggiolesi
Keyword(s):  
Intuitionistic Logic ◽  
Logic Of Proofs

scholarly journals On the correspondence between nested calculi and semantic systems for intuitionistic logics

2020 ◽  
Author(s):  
Tim Lyon
Keyword(s):  
Intuitionistic Logic ◽  
Structural Rules ◽  
First Order ◽  
Constant Domains ◽  
The Relationship ◽  
Intuitionistic Logics

Abstract This paper studies the relationship between labelled and nested calculi for propositional intuitionistic logic, first-order intuitionistic logic with non-constant domains and first-order intuitionistic logic with constant domains. It is shown that Fitting’s nested calculi naturally arise from their corresponding labelled calculi—for each of the aforementioned logics—via the elimination of structural rules in labelled derivations. The translational correspondence between the two types of systems is leveraged to show that the nested calculi inherit proof-theoretic properties from their associated labelled calculi, such as completeness, invertibility of rules and cut admissibility. Since labelled calculi are easily obtained via a logic’s semantics, the method presented in this paper can be seen as one whereby refined versions of labelled calculi (containing nested calculi as fragments) with favourable properties are derived directly from a logic’s semantics.

scholarly journals On Correspondence between Selective CPS Transformation and Selective Double Negation Translation

Mathematics ◽  
2021 ◽  
Vol 9 (4) ◽  
pp. 385
Author(s):  
Hyeonseung Im
Keyword(s):  
Programming Languages ◽  
Intuitionistic Logic ◽  
Reference Point ◽  
Classical Logic ◽  
Proof System ◽  
Double Negation

A double negation translation (DNT) embeds classical logic into intuitionistic logic. Such translations correspond to continuation passing style (CPS) transformations in programming languages via the Curry-Howard isomorphism. A selective CPS transformation uses a type and effect system to selectively translate only nontrivial expressions possibly with computational effects into CPS functions. In this paper, we review the conventional call-by-value (CBV) CPS transformation and its corresponding DNT, and provide a logical account of a CBV selective CPS transformation by defining a selective DNT via the Curry-Howard isomorphism. By using an annotated proof system derived from the corresponding type and effect system, our selective DNT translates classical proofs into equivalent intuitionistic proofs, which are smaller than those obtained by the usual DNTs. We believe that our work can serve as a reference point for further study on the Curry-Howard isomorphism between CPS transformations and DNTs.

Introducing Justification into Epistemic Logic

2005 ◽  
Vol 15 (6) ◽  
pp. 1059-1073 ◽  
Author(s):  
Sergei Artemov ◽  
Elena Nogina
Keyword(s):  
Epistemic Logic
Sign in / Sign up

Export Citation Format

Share Document