scholarly journals Formalization of the Equivalence among Completeness Theorems of Real Number in Coq

Mathematics ◽  
2020 ◽  
Vol 9 (1) ◽  
pp. 38
Author(s):  
Yaoshun Fu ◽  
Wensheng Yu
Keyword(s):  
Real Number ◽  
Fundamental Theorem ◽  
Completeness Theorem ◽  
Accumulation Point ◽  
Formal Proof ◽  
Theorem Prover ◽  
Monotone Convergence ◽  
Formalization Of Mathematics ◽  
Sequential Compactness ◽  
Completeness Theorems

The formalization of mathematics based on theorem prover becomes increasingly important in mathematics and computer science, and, particularly, formalizing fundamental mathematical theories becomes especially essential. In this paper, we describe the formalization in Coq of eight very representative completeness theorems of real numbers. These theorems include the Dedekind fundamental theorem, Supremum theorem, Monotone convergence theorem, Nested interval theorem, Finite cover theorem, Accumulation point theorem, Sequential compactness theorem, and Cauchy completeness theorem. We formalize the real number theory strictly following Landau’s Foundations of Analysis where the Dedekind fundamental theorem can be proved. We extend this system and complete the related notions and properties for finiteness and sequence. We prove these theorems in turn from Dedekind fundamental theorem, and finally prove the Dedekind fundamental theorem by the Cauchy completeness theorem. The full details of formal proof are checked by the proof assistant Coq, which embodies the characteristics of reliability and interactivity. This work can lay the foundation for many applications, especially in calculus and topology.

On the strong semantical completeness of the intuitionistic predicate calculus

1968 ◽  
Vol 33 (1) ◽  
pp. 1-7 ◽  
Author(s):  
Richmond H. Thomason
Keyword(s):  
Model Theory ◽  
Completeness Theorem ◽  
Predicate Calculus ◽  
First Order ◽  
Semantic Tableaux ◽  
Weak Completeness ◽  
Skolem Theorem ◽  
Completeness Theorems

In Kripke [8] the first-order intuitionjstic predicate calculus (without identity) is proved semantically complete with respect to a certain model theory, in the sense that every formula of this calculus is shown to be provable if and only if it is valid. Metatheorems of this sort are frequently called weak completeness theorems—the object of the present paper is to extend Kripke's result to obtain a strong completeness theorem for the intuitionistic predicate calculus of first order; i.e., we will show that a formula A of this calculus can be deduced from a set Γ of formulas if and only if Γ implies A. In notes 3 and 5, below, we will indicate how to account for identity, as well. Our proof of the completeness theorem employs techniques adapted from Henkin [6], and makes no use of semantic tableaux; this proof will also yield a Löwenheim-Skolem theorem for the modeling.

scholarly journals Transition of Consistency and Satisfiability under Language Extensions

2012 ◽  
Vol 20 (3) ◽  
pp. 193-197
Author(s):  
Julian J. Schlöder ◽  
Peter Koepke
Keyword(s):  
Present Article ◽  
Formal Languages ◽  
Completeness Theorem ◽  
Formal Proof

Summary This article is the first in a series of two Mizar articles constituting a formal proof of the Gödel Completeness theorem [17] for uncountably large languages. We follow the proof given in [18]. The present article contains the techniques required to expand formal languages. We prove that consistent or satisfiable theories retain these properties under changes to the language they are formulated in.

Proof theory

2004 ◽  
Author(s):  
Shawn Hedman
Keyword(s):  
Propositional Logic ◽  
Completeness Theorem ◽  
Formal Proof ◽  
Order Logic ◽  
Truth Table ◽  
First Order Logic ◽  
Formal Proofs ◽  
Systematic Method ◽  
First Order

As with any logic, the semantics of first-order logic yield rules for deducing the truth of one sentence from that of another. In this chapter, we develop both formal proofs and resolution for first-order logic. As in propositional logic, each of these provides a systematic method for proving that one sentence is a consequence of another. Recall the Consequence problem for propositional logic. Given formulas F and G, the problemis to decide whether or not G is a consequence of F. From Chapter 1, we have three approaches to this problem: • We could compute the truth table for the formula F → G. If the truth values are all 1s then we conclude that F → G is a tautology and G is a consequence of F. Otherwise, G is not a consequence of F. • Using Tables 1.5 and 1.6, we could try to formally derive G from {F}. By the Completeness Theorem for propositional logic, G is a consequence of F if and only if {F} ├ G. • We could use resolution. By Theorem1.76, G is a consequence of F if and only if ∅ ∈ Res(H) where H is a formula in CNF equivalent to (F ∧￢G). Using these methods not only can we determine whether one formula is a consequence of another, but also we can determine whether a given formula is a tautology or a contradiction. A formula F is a tautology if and only if F is a consequence of (A∨￢A) if and only if ￢F is a contradiction. In this chapter, we consider the analogous problems for first-order logic. Given formulas φ and ψ, how can we determine whether ψ is a consequence of φ? Equivalently, how can we determine whether a given formula is a tautology or a contradiction? We present three methods for answering these questions. • In Section 3.1, we define a notion of formal proof for first-order logic by extending Table 1.5. • In Section 3.3, we “reduce” formulas of first-order logic to sets of formulas of propositional logic where we use resolution as defined in Chapter 1.

Axioms of symmetry: Throwing darts at the real number line

1986 ◽  
Vol 51 (1) ◽  
pp. 190-200 ◽  
Author(s):  
Chris Freiling
Keyword(s):  
Real Number ◽  
Lebesgue Measure ◽  
Thought Experiment ◽  
Continuum Hypothesis ◽  
Number Line ◽  
Formal Proof ◽  
The Real ◽  
Joint Measurability ◽  
The Axiom Of Choice ◽  
Real Number Line

AbstractWe will give a simple philosophical “proof” of the negation of Cantor's continuum hypothesis (CH). (A formal proof for or against CH from the axioms of ZFC is impossible; see Cohen [1].) We will assume the axioms of ZFC together with intuitively clear axioms which are based on some intuition of Stuart Davidson and an old theorem of Sierpiński and are justified by the symmetry in a thought experiment throwing darts at the real number line. We will in fact show why there must be an infinity of cardinalities between the integers and the reals. We will also show why Martin's Axiom must be false, and we will prove the extension of Fubini's Theorem for Lebesgue measure where joint measurability is not assumed. Following the philosophy—if you reject CH you are only two steps away from rejecting the axiom of choice (AC)—we will point out along the way some extensions of our intuition which contradict AC.

A unified completeness theorem for quantified modal logics

2002 ◽  
Vol 67 (4) ◽  
pp. 1483-1510 ◽  
Author(s):  
Giovanna Corsi
Keyword(s):  
Modal Logic ◽  
Completeness Theorem ◽  
Modal Logics ◽  
General Strategy ◽  
Quantified Modal Logic ◽  
Barcan Formula ◽  
Completeness Theorems

AbstractA general strategy for proving completeness theorems for quantified modal logics is provided. Starting from free quantified modal logic K. with or without identity, extensions obtained either by adding the principle of universal instantiation or the converse of the Barcan formula or the Barcan formula are considered and proved complete in a uniform way. Completeness theorems are also shown for systems with the extended Barcan rule as well as for some quantified extensions of the modal logic B. The incompleteness of Q°.B + BF is also proved.

INDUCTION-ORIENTED VERIFICATION OF REPLICATED ARCHITECTURES DESCRIBED IN VHDL

2000 ◽  
Vol 10 (03n04) ◽  
pp. 181-204
Author(s):  
LAURENCE PIERRE
Keyword(s):  
Computer Aided Design ◽  
Formal Proof ◽  
Theorem Prover ◽  
Hardware Description Languages ◽  
One Dimensional ◽  
Functional Representation ◽  
Hardware Description ◽  
Proof Techniques ◽  
Description Languages ◽  
Aided Design

This paper is concerned with the application of theorem proving techniques to the formal proof of hardware. More precisely, we aim at providing a methodology for applying provers like Nqthm or Acl2 to the formal verification of parameterized replicated circuits. Nqthm (the Boyer–Moore theorem prover) and its successor Acl2 are induction-based systems; their formalisms are respectively a simplified Lisp-like language and Common Lisp. Hence, the circuits we consider must be given a purely functional representation. Moreover, our work puts the emphasis on the integration of formal proof techniques in CAD (Computer Aided Design) environments which support Hardware Description Languages in which replication is expressed by iteration. Therefore, we associate with the iterative statement of the VHDL language a functional semantics that guarantees an easy translation from VHDL to Nqthm/Acl2 while simplifying the subsequent inductive proofs. The approach has been successfully applied to one-dimensional as well as two-dimensional structures.

Adding propositional connectives to countable infinitary logic

1975 ◽  
Vol 77 (1) ◽  
pp. 1-6
Author(s):  
Harvey Friedman
Keyword(s):  
Completeness Theorem ◽  
Predicate Calculus ◽  
Compactness Theorem ◽  
Functional Completeness ◽  
Infinitary Logic ◽  
Completeness Theorems ◽  
Infinite Sequences

AbstractFor countable admissible α, one can add a new infinitary propositional connective to so that the extended language obeys the Barwise compactness theorem, and the set of valid sentences is complete α-r.e.Aside from obeying the compactness theorem and a completeness theorem, ordinary finitary predicate calculus is also truth-functionally complete.In (1), Barwise shows that for countable admissible A, provides a fragment of which obeys a compactness theorem and a completeness theorem. However, we of course lose truth-functional completeness, with respect to infinitary propositional connectives that operate on infinite sequences of propositional variables. This raises the question of studying extensions of the language obtained by adding infinitary propositional connectives, in connexion with the Barwise compactness and completeness theorems, and other metatheorems, proved for Some aspects of this project are proposed in (3). It is the purpose of this paper to answer a few of the more basic questions which arise in this connexion.We have not attempted to study the preservation of interpolation or implicit definability. This could be quite interesting if done systematically.

scholarly journals Notes on Recent Achievements in Proving Stability using KeYmaeraX

2021 ◽  
Vol 28 (4) ◽  
pp. 326-336
Author(s):  
Thomas Baar ◽  
Horst Schulte
Keyword(s):  
Asymptotic Stability ◽  
Closed Loop ◽  
Continuous System ◽  
Formal Proof ◽  
Theorem Prover ◽  
Closed Loop Control ◽  
Continuous Variables ◽  
Formal Proofs ◽  
Open Problems ◽  
Loop Control

KeYmaeraX is a Hoare-style theorem prover for hybrid systems. A hybrid system can be seen as an aggregation of both discrete and continuous variables, whose values can change abruptly or continuously, respectively. KeYmaeraX supports only variables having the primitive type bool or real. Due to the mixture of discrete and continuous system elements, one promising application area for KeYmaeraX are closed-loop control systems. A closed-loop control system consists of a plant and a controller. While the plant is basically an aggregation of continuous variables whose values change over time accordingly to physical laws, the controller can be seen as an algorithm formulated in a classical programming language. In this paper, we review some recent extensions of the proof calculus applied by KeYmaeraX that make formal proofs on the stability of dynamic systems more feasible. Based on an example, we first introduce to the topic and prove asymptotic stability of a given system in a hand-written mathematical style. This approach is then compared with a formal encoding of the problem and a formal proof established in KeYmaeraX. We also discuss open problems such as the formalization of asymptotic stability.

On Small Complete Sets of Functions

2000 ◽  
Vol 52 (1) ◽  
pp. 3-30 ◽  
Author(s):  
Lev Aizenberg ◽  
Alekos Vidras
Keyword(s):  
Holomorphic Functions ◽  
Direct Consequence ◽  
Completeness Theorem ◽  
Duality Principle ◽  
Residue Theorem ◽  
Complete Sets ◽  
Local Residues ◽  
Completeness Theorems

AbstractUsing Local Residues and the Duality Principle a multidimensional variation of the completeness theorems by T. Carleman and A. F. Leontiev is proven for the space of holomorphic functions defined on a suitable open strip Tα ⊂ C2. The completeness theorem is a direct consequence of the Cauchy Residue Theorem in a torus. With suitable modifications the same result holds in Cn.

Sign in / Sign up

Export Citation Format

Share Document