Proofs and surfaces

A formal sequent system dealing with Menelaus' configurations is introduced in this paper. The axiomatic sequents of the system stem from 2-cycles of Δ-complexes. The Euclidean and projective interpretations of the sequents are defined and a soundness result is proved. This system is decidable and its provable sequents deliver incidence results. A cyclic operad structure tied to this system is presented by generators and relations.     

Proofs and Countermodels in Non-Classical Logics

Proofs and countermodels are the two sides of completeness proofs, but, in general, failure to find one does not automatically give the other. The limitation is encountered also for decidable non-classical logics in traditional completeness proofs based on Henkin’s method of maximal consistent sets of formulas. A method is presented that makes it possible to establish completeness in a direct way: For any given sequent either a proof in the given logical system or a countermodel in the corresponding frame class is found. The method is a synthesis of a generation of calculi with internalized relational semantics, a Tait–Schütte–Takeuti style completeness proof, and procedures to finitize the countermodel construction. Finitizations for intuitionistic propositional logic are obtained through the search for a minimal derivation, through pruning of infinite branches in search trees by means of a suitable syntactic counterpart of semantic filtration, or through a proof-theoretic embedding into an appropriate provability logic. A number of examples illustrates the method, its subtleties, challenges, and present scope.     

Hypothetical Logic of Proofs

The logic of proofs is a refinement of modal logic introduced by Artemov in 1995 in which the modality ?A is revisited as ?t?A where t is an expression that bears witness to the validity of A. It enjoys arithmetical soundness and completeness and is capable of reflecting its own proofs (?A implies ? ?t?A, for some t). We develop the Hypothetical Logic of Proofs, a reformulation of LP based on judgemental reasoning.     

Proofs with monotone cuts

Atserias, Galesi, and Pudlák have shown that the monotone sequent calculus MLK quasipolynomially simulates proofs of monotone sequents in the full sequent calculus LK (or equivalently, in Frege systems). We generalize the simulation to the fragment MCLK of LK which can prove arbitrary sequents, but restricts cut‐formulas to be monotone. We also show that MLK as a refutation system for CNFs quasipolynomially simulates LK.     

Other Proofs of Old Results

We transform the proof of the second incompleteness theorem given in [3] to a proof-theoretic version, avoiding the use of the arithmetized completeness theorem. We give also new proofs of old results: The Arithmetical Hierarchy Theorem and Tarski's Theorem on undefinability of truth; the proofs in which the construction of a sentence by means of diagonalization lemma is not needed.     

Preservice Teacher Beliefs About Proofs

This article describes a study of backgrounds, beliefs, and attitudes of teachers about proofs. Thirty preservice elementary teachers enrolled in a mathematics content course and 21 secondary mathematics teachers in an abstract algebra course were surveyed. The study explored four issues: preservice teachers' experiences/exposure to proof, their beliefs about what constitutes a proof and the role of proof in mathematics, and their beliefs about when proof should be introduced in grades K-12. Results of the survey are described as a means for discussing the backgrounds and beliefs future teachers hold with regard to teaching proofs in their own classrooms. Finally, a short collection of sample explorations and questions, which could be used to encourage the thinking and writing of proofs in grades K-12, is provided. One of these questions was posed to 215 secondary students; examples of their reasoning and a discussion of the various techniques employed by the students are included.     

Possible Student Justification of Proofs

The National Council of Teachers of Mathematics calls for an increased emphasis on proof and reasoning in school mathematics curricula. Given such an emphasis, mathematics teachers must be prepared to structure curricular experiences so that students develop an appreciation for both the value of proof and for those strategies that will assist them in developing proving skills. Such an outcome is more likely when the teacher feels secure in his/her own understanding of the concept of “mathematical proof” and understands the ways in which students progress as they take on increasingly more complex mathematical justifications. In this article, a model of mathematical proof, based on Balacheff's Taxonomy of Mathematical Proof, outlining the levels through which students might progress as they develop proving skills is discussed. Specifically, examples of the various ways in which students operating at different levels of skill sophistication could approach three different mathematical proof tasks are presented. By considering proofs under this model, teachers are apt to gain a better understanding of each student's entry skill level and so effectively guide him/her toward successively more sophisticated skill development.     

Structuring Co-constructive Logic for Proofs and Refutations

This paper considers a topos-theoretic structure for the interpretation of co-constructive logic for proofs and refutations following Trafford (Studia Humana 3(4):22–40, 2015). It is notoriously tricky to define a proof-theoretic semantics for logics that adequately represent constructivity over proofs and refutations. By developing abstractions of elementary topoi, we consider an elementary topos as structure for proofs, and complement topos as structure for refutation. In doing so, it is possible to consider a dialogue structure between these topoi, and also control their relation such that classical logic (interpreted in a Boolean topos) is simulated where proofs and refutations are conclusive.     

Prototype Proofs in Type Theory

The proofs of universally quantified statements, in mathematics, are given as “schemata” or as “prototypes” which may be applied to each specific instance of the quantified variable. Type Theory allows to turn into a rigorous notion this informal intuition described by many, including Herbrand. In this constructive approach where propositions are types, proofs are viewed as terms of λ‐calculus and act as “proof‐schemata”, as for universally quantified types. We examine here the critical case of Impredicative Type Theory, i. e. Girard's system F, where type‐quantification ranges over all types. Coherence and decidability properties are proved for prototype proofs in this impredicative context.     

Extracting Algorithms from Intuitionistic Proofs

This paper presents a new method - which does not rely on the cut-elimination theorem - for characterizing the provably total functions of certain intuitionistic subsystems of arithmetic. The new method hinges on a realizability argument within an infinitary language. We illustrate the method for the intuitionistic counterpart of Buss's theory S, and we briefly sketch it for the other levels of bounded arithmetic and for the theory IΣ₁.     

一个不等式的三种证明

针对某教材中关于凹函数不等式的一道证明题,分别采用单调性、泰勒公式和中值定理给出三种证明方法,旨在帮助学生拓展其思维广度,培养其综合能力,提高其数学素质．     

一个命题的多种证明

在解答某文献中的一个问题的过程中,得到了一个命题.用不同的方法给出了该名题的多种证明.     

微分学中不等式的证明

针对微分学不等式列出五种常用证明方法,即利用单调性证明法,利用拉格朗日中值定理证明法,利用最值证明法,利用泰勒公式证明法,和利用凹凸性证明法.实例说明每种方法的使用细节,以达到使初学者能尽快掌握微分学不等式证明的目的.