Elementary axioms for canonical points of toposes

1987 ◽  
Vol 52 (1) ◽  
pp. 202-204
Author(s):  
Colin McLarty
Keyword(s):  
Geometric Meaning ◽  
Law Of Excluded Middle ◽  
The Law ◽  
Excluded Middle ◽  
Geometric Morphism

Two elementary extensions of the topos axioms are given, each implying the topos has a local geometric morphism to a category of sets. The stronger one realizes sets as precisely the decidables of the topos, so there is a simple internal description of the range of validity of the law of excluded middle in the topos. It also has a natural geometric meaning. Models of the extensions in Grothendieck toposes are described.

Reconsidering Kant’s Rejection of Indirect Arguments in Transcendental Philosophy

2021 ◽  
pp. 1-19
Author(s):  
Marcel Buß
Keyword(s):  
Immanuel Kant ◽  
Explanatory Power ◽  
Transcendental Philosophy ◽  
Point Of View ◽  
Transcendental Arguments ◽  
Mathematical Proofs ◽  
Law Of Excluded Middle ◽  
The Law ◽  
Excluded Middle ◽  
Insight Into

Abstract Immanuel Kant states that indirect arguments are not suitable for the purposes of transcendental philosophy. If he is correct, this affects contemporary versions of transcendental arguments which are often used as an indirect refutation of scepticism. I discuss two reasons for Kant’s rejection of indirect arguments. Firstly, Kant argues that we are prone to misapply the law of excluded middle in philosophical contexts. Secondly, Kant points out that indirect arguments lack some explanatory power. They can show that something is true but they do not provide insight into why something is true. Using mathematical proofs as examples, I show that this is because indirect arguments are non-constructive. From a Kantian point of view, transcendental arguments need to be constructive in some way. In the last part of the paper, I briefly examine a comment made by P. F. Strawson. In my view, this comment also points toward a connection between transcendental and constructive reasoning.

On Weakening the Law of Excluded Middle

Dialogue ◽  
1966 ◽  
Vol 5 (2) ◽  
pp. 232-236
Author(s):  
Douglas Odegard
Keyword(s):  
Law Of Excluded Middle ◽  
The Law ◽  
Excluded Middle

Let us use ‘false’ and ‘not true’ (and cognates) in such a way that the latter expression covers the broader territory of the two; in other words, a statement's falsity implies its non-truth but not vice versa. For example, ‘John is ill’ cannot be false without being nontrue; but it can be non-true without being false, since it may not be true when ‘John is not ill’ is also not true, a situation we could describe by saying ‘It is neither the case that John is ill nor the case that John is not ill.’

The Law of Excluded Middle

Mind ◽  
1978 ◽  
Vol LXXXVII (2) ◽  
pp. 161-180 ◽  
Author(s):  
NEIL COOPER
Keyword(s):  
Law Of Excluded Middle ◽  
The Law ◽  
Excluded Middle

Frege's theorem in a constructive setting

1999 ◽  
Vol 64 (2) ◽  
pp. 486-488 ◽  
Author(s):  
John L. Bell
Keyword(s):  
Set Theory ◽  
Natural Numbers ◽  
The Family ◽  
Power Set ◽  
Law Of Excluded Middle ◽  
The Law ◽  
Image Position ◽  
Excluded Middle ◽  
Intuitionistic Set Theory

By Frege's Theorem is meant the result, implicit in Frege's Grundlagen, that, for any set E, if there exists a map υ from the power set of E to E satisfying the conditionthen E has a subset which is the domain of a model of Peano's axioms for the natural numbers. (This result is proved explicitly, using classical reasoning, in Section 3 of [1].) My purpose in this note is to strengthen this result in two directions: first, the premise will be weakened so as to require only that the map υ be defined on the family of (Kuratowski) finite subsets of the set E, and secondly, the argument will be constructive, i.e., will involve no use of the law of excluded middle. To be precise, we will prove, in constructive (or intuitionistic) set theory, the followingTheorem. Let υ be a map with domain a family of subsets of a set E to E satisfying the following conditions:(i) ø ϵdom(υ)(ii)∀U ϵdom(υ)∀x ϵ E − UU ∪ x ϵdom(υ)(iii)∀UV ϵdom(5) υ(U) = υ(V) ⇔ U ≈ V.Then we can define a subset N of E which is the domain of a model of Peano's axioms.

scholarly journals Validating Brouwer's continuity principle for numbers using named exceptions

2017 ◽  
Vol 28 (6) ◽  
pp. 942-990 ◽  
Author(s):  
VINCENT RAHLI ◽  
MARK BICKFORD
Keyword(s):  
Equivalence Relation ◽  
Dependent Types ◽  
Proof Assistant ◽  
Continuity Theorem ◽  
Continuity Principle ◽  
Fan Theorem ◽  
Law Of Excluded Middle ◽  
The Law ◽  
Intuitionistic Mathematics ◽  
Excluded Middle

This paper extends the Nuprl proof assistant (a system representative of the class of extensional type theories with dependent types) withnamed exceptionsandhandlers, as well as a nominalfreshoperator. Using these new features, we prove a version of Brouwer's continuity principle for numbers. We also provide a simpler proof of a weaker version of this principle that only uses diverging terms. We prove these two principles in Nuprl's metatheory using our formalization of Nuprl in Coq and reflect these metatheoretical results in the Nuprl theory as derivation rules. We also show that these additions preserve Nuprl's key metatheoretical properties, in particular consistency and the congruence of Howe's computational equivalence relation. Using continuity and the fan theorem, we prove important results of Intuitionistic Mathematics: Brouwer's continuity theorem, bar induction on monotone bars and the negation of the law of excluded middle.

A proof–technique in uniform space theory

2003 ◽  
Vol 68 (3) ◽  
pp. 795-802 ◽  
Author(s):  
Douglas Bridges ◽  
Luminiţa Vîţă
Keyword(s):  
Uniform Space ◽  
Weak Form ◽  
Space Theory ◽  
Proof Technique ◽  
Uniform Spaces ◽  
Constructive Theory ◽  
Law Of Excluded Middle ◽  
The Law ◽  
Excluded Middle

AbstractIn the constructive theory of uniform spaces there occurs a technique of proof in which the application of a weak form of the law of excluded middle is circumvented by purely analytic means. The essence of this proof–technique is extracted and then applied in several different situations.

Core Logic and the Paradoxes

2017 ◽  
Author(s):  
Neil Tennant
Keyword(s):  
Normal Form ◽  
Set Theory ◽  
Free Logic ◽  
Semantic Paradoxes ◽  
Law Of Excluded Middle ◽  
The Law ◽  
The Liar ◽  
Excluded Middle

The Law of Excluded Middle is not to be blamed for any of the logico-semantic paradoxes. We explain and defend our proof-theoretic criterion of paradoxicality, according to which the ‘proofs’ of inconsistency associated with the paradoxes are in principle distinct from those that establish genuine inconsistencies, in that they cannot be brought into normal form. Instead, the reduction sequences initiated by paradox-posing proofs ‘of ⊥’ do not terminate. This criterion is defended against some recent would-be counterexamples by stressing the need to use Core Logic’s parallelized forms of the elimination rules. We show how Russell’s famous paradox in set theory is not a genuine paradox; for it can be construed as a disproof, in the free logic of sets, of the assumption that the set of all non-self-membered sets exists. The Liar (by contrast) is still paradoxical, according to the proof-theoretic criterion of paradoxicality.

Sign in / Sign up

Export Citation Format

Share Document