scholarly journals Intuitionistic completeness for first order classical logic

1999 ◽  
Vol 64 (1) ◽  
pp. 304-312 ◽  
Author(s):  
Stefano Berardi
Keyword(s):  
Intuitionistic Logic ◽  
Classical Logic ◽  
First Order ◽  
The Past

AbstractIn the past sixty years or so, a real forest of intuitionistic models for classical theories has grown. In this paper we will compare intuitionistic models of first order classical theories according to relevant issues, like completeness (w.r.t. first order classical provability), consistency, and relationship between a connective and its interpretation in a model. We briefly consider also intuitionistic models for classical ω-logic.All results included here, but a part of the proposition (a) below, are new. This work is, ideally, a continuation of a paper by McCarty, who considered intuitionistic completeness mostly for first order intuitionistic logic.

An embedding of classical logic in S4

1970 ◽  
Vol 35 (4) ◽  
pp. 529-534 ◽  
Author(s):  
Melvin Fitting
Keyword(s):  
Intuitionistic Logic ◽  
Model Theory ◽  
Classical Logic ◽  
First Order ◽  
Barcan Formula ◽  
Complete Sequences

There are well-known embeddings of intuitionistic logic into S4 and of classical logic into S5. In this paper we give a related embedding of (first order) classical logic directly into (first order) S4, with or without the Barcan formula. If one reads the necessity operator of S4 as ‘provable’, the translation may be roughly stated as: truth may be replaced by provable consistency. A proper statement will be found below. The proof is based ultimately on the notion of complete sequences used in Cohen's technique of forcing [1], and is given in terms of Kripke's model theory [3], [4].

An intuitionistically plausible interpretation of intuitionistic logic

1977 ◽  
Vol 42 (4) ◽  
pp. 564-578 ◽  
Author(s):  
H. C. M. de Swart
Keyword(s):  
Intuitionistic Logic ◽  
Predicate Calculus ◽  
Mathematical Treatment ◽  
First Order ◽  
The Past ◽  
Definition Of ◽  
Image Position ◽  
Order Predicate Calculus ◽  
Made In

Let IPC be the intuitionistic first-order predicate calculus. From the definition of derivability in IPC the following is clear:(1) If A is derivable in IPC, denoted by “⊦IPCA”, then A is intuitively true, that means, true according to the intuitionistic interpretation of the logical symbols. To be able to settle the converse question: “if A is intuitively true, then ⊦IPCA”, one should make the notion of intuitionistic truth more easily amenable to mathematical treatment. So we have to look then for a definition of “A is valid”, denoted by “⊨A”, such that the following holds:(2) If A is intuitively true, then ⊨ A.Then one might hope to be able to prove(3) If ⊨ A, then ⊦IPCA.If one would succeed in finding a notion of “⊨ A”, such that all the conditions (1), (2) and (3) are satisfied, then the chain would be closed, i.e. all the arrows in the scheme below would hold.Several suggestions for ⊨ A have been made in the past: Topological and algebraic interpretations, see Rasiowa and Sikorski [1]; the intuitionistic models of Beth, see [2] and [3]; the interpretation of Grzegorczyk, see [4] and [5]; the models of Kripke, see [6] and [7]. In Thirty years of foundational studies, A. Mostowski [8] gives a review of the interpretations, proposed for intuitionistic logic, on pp. 90–98.

scholarly journals Dialogues for proof search

10.29007/5t86 ◽  
2018 ◽  
Author(s):  
Jesse Alama
Keyword(s):  
Intuitionistic Logic ◽  
Classical Logic ◽  
Order Logic ◽  
Theorem Prover ◽  
First Order Logic ◽  
Dialogue Games ◽  
First Order ◽  
Proof Search ◽  
Automated Theorem Prover

Dialogue games are a two-player semantics for a variety of logics, including intuitionistic and classical logic. Dialogues can be viewed as a kind of analytic calculus not unlike tableaux. Can dialogue games be an effective foundation for proof search in intuitionistic logic (both first-order and propositional)? We announce Kuno, an automated theorem prover for intuitionistic first-order logic based on dialogue games.

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.

scholarly journals Mathematical Creativity in Adults: Its Measurement and Its Relation to Intelligence, Mathematical Competence and General Creativity

2021 ◽  
Vol 9 (1) ◽  
pp. 10
Author(s):  
Michaela A. Meier ◽  
Julia A. Burgstaller ◽  
Mathias Benedek ◽  
Stephan E. Vogel ◽  
Roland H. Grabner
Keyword(s):  
Exploratory Study ◽  
Mathematical Creativity ◽  
Good Reliability ◽  
Mathematical Competence ◽  
First Order ◽  
The Past ◽  
Confirmatory Factor ◽  
Order Factor ◽  
General Creativity ◽  
Creativity Measure

Mathematical creativity is perceived as an increasingly important aspect of everyday life and, consequently, research has increased over the past decade. However, mathematical creativity has mainly been investigated in children and adolescents so far. Therefore, the first goal of the current study was to develop a mathematical creativity measure for adults (MathCrea) and to evaluate its reliability and construct validity in a sample of 100 adults. The second goal was to investigate how mathematical creativity is related to intelligence, mathematical competence, and general creativity. The MathCrea showed good reliability, and confirmatory factor analysis confirmed that the data fitted the assumed theoretical model, in which fluency, flexibility, and originality constitute first order factors and mathematical creativity a second order factor. Even though intelligence, mathematical competence, and general creativity were positively related to mathematical creativity, only numerical intelligence and general creativity predicted unique variance of mathematical creativity. Additional analyses separating quantitative and qualitative aspects of mathematical creativity revealed differential relationships to intelligence components and general creativity. This exploratory study provides first evidence that intelligence and general creativity are important predictors for mathematical creativity in adults, whereas mathematical competence seems to be not as important for mathematical creativity in adults as in children.

Old and New Results for First Order Periodic ODEs without Uniqueness: a Comprehensive Study by Lower and Upper Solutions

2004 ◽  
Vol 4 (3) ◽  
Author(s):  
Franco Obersnel ◽  
Pierpaolo Omari
Keyword(s):  
Cauchy Problem ◽  
Differential Equations ◽  
Lower And Upper Solutions ◽  
Elementary Approach ◽  
Qualitative Properties ◽  
First Order ◽  
The Past ◽  
The Cauchy Problem ◽  
Qualitative Properties Of Solutions ◽  
Comprehensive Study

AbstractAn elementary approach, based on a systematic use of lower and upper solutions, is employed to detect the qualitative properties of solutions of first order scalar periodic ordinary differential equations. This study is carried out in the Carathéodory setting, avoiding any uniqueness assumption, in the future or in the past, for the Cauchy problem. Various classical and recent results are recovered and generalized.

scholarly journals Memory and reflection

2021 ◽  
Vol 44 (spe2) ◽  
pp. 151-168
Author(s):  
Chienkuo Mi
Keyword(s):  
Problem Solving ◽  
Virtue Epistemology ◽  
Animal Cognition ◽  
Active Role ◽  
Careful Examination ◽  
First Order ◽  
The Past ◽  
The Analects ◽  
Normative Status ◽  
Previous Learning

Abstract: I have argued that the Analects of Confucius presents us with a conception of reflection with two components, a retrospective component and a perspective component. The former component involves hindsight or careful examination of the past and as such draws on previous learning or memory and previously formed beliefs to avoid error. The latter component is foresight, or forward looking, and as such looks to existing beliefs and factors in order to achieve knowledge. In this paper, I raise the problem of forgetting and argue that most of contemporary theories of knowledge have to face the problem and deal with the challenge seriously. In order to solve the problem, I suggest a bi-level virtue epistemology which can provide us with the best outlook for the problem-solving. I will correlate two different cognitive capacities or processes of “memory” (and “forgetting”) with the conception of reflection, and evaluate them under two different frameworks, a strict deontic framework (one that presupposes free and intentional determination) and a more loosely deontic framework (one that highlights functional and mechanical faculties). The purpose is to show that reflection as meta-cognition plays an important and active role and enjoys a better epistemic (normative) status in our human endeavors (cognitive or epistemic) than those of first-order (or animal) cognition, such as memory, can play.

scholarly journals On density of truth of the intuitionistic logic in one variable

2008 ◽  
Vol DMTCS Proceedings vol. AI,... (Proceedings) ◽  
Author(s):  
Zofia Kostrzycka
Keyword(s):  
Intuitionistic Logic ◽  
Classical Logic ◽  
Propositional Logic ◽  
Propositional Variable ◽  
Intuitionistic Propositional Logic ◽  
International Audience

International audience In this paper we focus on the intuitionistic propositional logic with one propositional variable. More precisely we consider the standard fragment $\{ \to ,\vee ,\bot \}$ of this logic and compute the proportion of tautologies among all formulas. It turns out that this proportion is different from the analog one in the classical logic case.

scholarly journals The exponential eigenmodes of the carbon-climate system, and their implications for ratios of responses to forcings

2013 ◽  
Vol 4 (1) ◽  
pp. 31-49 ◽  
Author(s):  
M. R. Raupach
Keyword(s):  
Linear Systems ◽  
Co2 Emissions ◽  
Radiative Forcing ◽  
Co2 Emission ◽  
Climate Model ◽  
Climate System ◽  
First Order ◽  
The Past ◽  
Emissions Scenarios ◽  
Co2 Sink

Abstract. Several basic ratios of responses to forcings in the carbon-climate system are observed to be relatively steady. Examples include the CO2 airborne fraction (the fraction of the total anthropogenic CO2 emission flux that accumulates in the atmosphere) and the ratio T/QE of warming (T) to cumulative total CO2 emissions (QE). This paper explores the reason for such near-constancy in the past, and its likely limitations in future. The contemporary carbon-climate system is often approximated as a set of first-order linear systems, for example in response-function descriptions. All such linear systems have exponential eigenfunctions in time (an eigenfunction being one that, if applied to the system as a forcing, produces a response of the same shape). This implies that, if the carbon-climate system is idealised as a linear system (Lin) forced by exponentially growing CO2 emissions (Exp), then all ratios of responses to forcings are constant. Important cases are the CO2 airborne fraction (AF), the cumulative airborne fraction (CAF), other CO2 partition fractions and cumulative partition fractions into land and ocean stores, the CO2 sink uptake rate (kS, the combined land and ocean CO2 sink flux per unit excess atmospheric CO2), and the ratio T/QE. Further, the AF and the CAF are equal. Since the Lin and Exp idealisations apply approximately to the carbon-climate system over the past two centuries, the theory explains the observed near-constancy of the AF, CAF and T/QE in this period. A nonlinear carbon-climate model is used to explore how future breakdown of both the Lin and Exp idealisations will cause the AF, CAF and kS to depart significantly from constancy, in ways that depend on CO2 emissions scenarios. However, T/QE remains approximately constant in typical scenarios, because of compensating interactions between CO2 emissions trajectories, carbon-climate nonlinearities (in land–air and ocean–air carbon exchanges and CO2 radiative forcing), and emissions trajectories for non-CO2 gases. This theory establishes a basis for the widely assumed proportionality between T and QE, and identifies the limits of this relationship.

Sign in / Sign up

Export Citation Format

Share Document