All accepted proofs of the Four Colour Theorem (4CT) are computer-dependent; and appeal to the existence, and manual identification, of an ‘unavoidable’ set containing a sufficient number of explicitly defined configurations—each evidenced only by a computer as ‘reducible’—such that at least one of the configurations must occur in any chromatically distinguished, minimal, planar map. For instance, Appel and Haken ‘identified’ 1,482 such configurations in their 1977, computer-dependent, proof of 4CT; whilst Neil Robertson et al ‘identified’ 633 configurations as sufficient in (...) their 1997, also computer-dependent, proof of 4CT. However, treating any specific number of ‘reducible’ configurations in an ‘unavoidable’ set as sufficient entails a minimum number as necessary and sufficient. We now show that the minimum number of such configurations can only be the one corresponding to the ‘unavoidable’ set of a ‘reducible’, 4-sided configuration identified by Alfred Kempe in his, seemingly fatally flawed, 1879 ‘proof’ of 4CT. Although Kempe appealed to putative properties of ‘Kempe’ chains in a graphical representation to fallaciously argue that a 5-sided configuration was also in the ‘unavoidable’ set, and ‘reducible’, we shall show why the flaw in his ‘proof’ is not fatal when the argument is expressed geometrically; and that, essentially, Kempe correctly argued that any planar map which admits a chromatic differentiation with a five-sided area C that shares non-zero boundaries with four, all differently coloured, neighbours can be 4-coloured. (shrink)

In this multi-disciplinary investigation we show how an evidence-based perspective of quantification---in terms of algorithmic verifiability and algorithmic computability---admits evidence-based definitions of well-definedness and effective computability, which yield two unarguably constructive interpretations of the first-order Peano Arithmetic PA---over the structure N of the natural numbers---that are complementary, not contradictory. The first yields the weak, standard, interpretation of PA over N, which is well-defined with respect to assignments of algorithmically verifiable Tarskian truth values to the formulas of PA under the interpretation. (...) The second yields a strong, finitary, interpretation of PA over N, which is well-defined with respect to assignments of algorithmically computable Tarskian truth values to the formulas of PA under the interpretation. We situate our investigation within a broad analysis of quantification vis a vis: * Hilbert's epsilon-calculus * Goedel's omega-consistency * The Law of the Excluded Middle * Hilbert's omega-Rule * An Algorithmic omega-Rule * Gentzen's Rule of Infinite Induction * Rosser's Rule C * Markov's Principle * The Church-Turing Thesis * Aristotle's particularisation * Wittgenstein's perspective of constructive mathematics * An evidence-based perspective of quantification. By showing how these are formally inter-related, we highlight the fragility of both the persisting, theistic, classical/Platonic interpretation of quantification grounded in Hilbert's epsilon-calculus; and the persisting, atheistic, constructive/Intuitionistic interpretation of quantification rooted in Brouwer's belief that the Law of the Excluded Middle is non-finitary. We then consider some consequences for mathematics, mathematics education, philosophy, and the natural sciences, of an agnostic, evidence-based, finitary interpretation of quantification that challenges classical paradigms in all these disciplines. (shrink)

All acknowledged proofs of the Four Colour Theorem (4CT) are computerdependent. They appeal to the existence, and manual identification, of an ‘unavoidable’ set containing a sufficient number of explicitly defined configurations—each evidenced only by a computer as ‘reducible’—such that at least one of the configurations must occur in any chromatically distinguished, putatively minimal, planar map. For instance, Appel and Haken ‘identified’ 1,482 such configurations in their 1977, computer-dependent, proof of 4CT; whilst Neil Robertson et al ‘identified’ 633 configurations as sufficient (...) in their 1997, also computer-dependent, proof of 4CT. However, treating any specific number of ‘reducible’ configurations in an ‘unavoidable’ set as sufficient entails a minimum number as necessary and sufficient. We now show that the minimum number of such configurations can only be the one corresponding to the ‘unavoidable’ set of the single, ‘reducible’, 4-sided configuration identified by Alfred Kempe in his, seemingly fatally flawed, 1879 ‘proof’ of 4CT. We shall further show that although Kempe fallaciously concluded that a 5-sided configuration was also in the ‘unavoidable’ set, and appealed to unproven properties of ‘Kempe’ chains in a graphical representation to then argue for its ‘reducibility’, neither flaw in his ‘proof’ is fatal when the argument is expressed geometrically; and that, essentially, Kempe correctly argued that any planar map which admits a chromatic differentiation with a five-sided area C that shares non-zero boundaries with four, all differently coloured, neighbours can be 4-coloured. (shrink)

We consider the argument that Tarski's classic definitions permit an intelligence---whether human or mechanistic---to admit finitary evidence-based definitions of the satisfaction and truth of the atomic formulas of the first-order Peano Arithmetic PA over the domain N of the natural numbers in two, hitherto unsuspected and essentially different, ways: (1) in terms of classical algorithmic verifiabilty; and (2) in terms of finitary algorithmic computability. We then show that the two definitions correspond to two distinctly different assignments of satisfaction and truth (...) to the compound formulas of PA over N---I_PA(N; SV ) and I_PA(N; SC). We further show that the PA axioms are true over N, and that the PA rules of inference preserve truth over N, under both I_PA(N; SV ) and I_PA(N; SC). We then show: (a) that if we assume the satisfaction and truth of the compound formulas of PA are always non-finitarily decidable under I_PA(N; SV ), then this assignment corresponds to the classical non-finitary putative standard interpretation I_PA(N; S) of PA over the domain N; and (b) that the satisfaction and truth of the compound formulas of PA are always finitarily decidable under the assignment I_PA(N; SC), from which we may finitarily conclude that PA is consistent. We further conclude that the appropriate inference to be drawn from Goedel's 1931 paper on undecidable arithmetical propositions is that we can define PA formulas which---under interpretation---are algorithmically verifiable as always true over N, but not algorithmically computable as always true over N. We conclude from this that Lucas' Goedelian argument is validated if the assignment I_PA(N; SV ) can be treated as circumscribing the ambit of human reasoning about `true' arithmetical propositions, and the assignment I_PA(N; SC) as circumscribing the ambit of mechanistic reasoning about `true' arithmetical propositions. (shrink)

In this multi-disciplinary investigation we show how an evidence-based perspective of quantification---in terms of algorithmic verifiability and algorithmic computability---admits evidence-based definitions of well-definedness and effective computability, which yield two unarguably constructive interpretations of the first-order Peano Arithmetic PA---over the structure N of the natural numbers---that are complementary, not contradictory. The first yields the weak, standard, interpretation of PA over N, which is well-defined with respect to assignments of algorithmically verifiable Tarskian truth values to the formulas of PA under the interpretation. (...) The second yields a strong, finitary, interpretation of PA over N, which is well-defined with respect to assignments of algorithmically computable Tarskian truth values to the formulas of PA under the interpretation. We situate our investigation within a broad analysis of quantification vis a vis: * Hilbert's epsilon-calculus * Goedel's omega-consistency * The Law of the Excluded Middle * Hilbert's omega-Rule * An Algorithmic omega-Rule * Gentzen's Rule of Infinite Induction * Rosser's Rule C * Markov's Principle * The Church-Turing Thesis * Aristotle's particularisation * Wittgenstein's perspective of constructive mathematics * An evidence-based perspective of quantification. By showing how these are formally inter-related, we highlight the fragility of both the persisting, theistic, classical/Platonic interpretation of quantification grounded in Hilbert's epsilon-calculus; and the persisting, atheistic, constructive/Intuitionistic interpretation of quantification rooted in Brouwer's belief that the Law of the Excluded Middle is non-finitary. We then consider some consequences for mathematics, mathematics education, philosophy, and the natural sciences, of an agnostic, evidence-based, finitary interpretation of quantification that challenges classical paradigms in all these disciplines. (shrink)

Classical interpretations of Goedels formal reasoning, and of his conclusions, implicitly imply that mathematical languages are essentially incomplete, in the sense that the truth of some arithmetical propositions of any formal mathematical language, under any interpretation, is, both, non-algorithmic, and essentially unverifiable. However, a language of general, scientific, discourse, which intends to mathematically express, and unambiguously communicate, intuitive concepts that correspond to scientific investigations, cannot allow its mathematical propositions to be interpreted ambiguously. Such a language must, therefore, define mathematical truth (...) verifiably. We consider a constructive interpretation of classical, Tarskian, truth, and of Goedel's reasoning, under which any formal system of Peano Arithmetic---classically accepted as the foundation of all our mathematical Languages---is verifiably complete in the above sense. We show how some paradoxical concepts of Quantum mechanics can, then, be expressed, and interpreted, naturally under a constructive definition of mathematical truth. (shrink)

Conventional wisdom dictates that proofs of mathematical propositions should be treated as necessary, and sufficient, for entailing `significant' mathematical truths only if the proofs are expressed in a---minimally, deemed consistent---formal mathematical theory in terms of: * Axioms/Axiom schemas * Rules of Deduction * Definitions * Lemmas * Theorems * Corollaries. Whilst Andrew Wiles' proof of Fermat's Last Theorem FLT, which appeals essentially to geometrical properties of real and complex numbers, can be treated as meeting this criteria, it nevertheless leaves two (...) questions unanswered: (i) Why is x^n +y^n = z^n solvable only for n < 3 if x, y, z, n are natural numbers? (ii) What technique might Fermat have used that led him to, even if only briefly, believe he had `a truly marvellous demonstration' of FLT? Prevailing post-Wiles wisdom---leaving (i) essentially unaddressed---dismisses Fermat's claim as a conjecture without a plausible proof of FLT. -/- However, we posit that providing evidence-based answers to both queries is necessary not only for treating FLT as significant, but also for understanding why FLT can be treated as a true arithmetical proposition. We thus argue that proving a theorem formally from explicit, and implicit, premises/axioms using rules of deduction---as currently accepted---is a meaningless game, of little scientific value, in the absence of evidence that has already established---unambiguously---why the premises/axioms and rules of deduction can be treated, and categorically communicated, as pre-formal truths in Marcus Pantsar's sense. Consequently, only evidence-based, pre-formal, truth can entail formal provability; and the formal proof of any significant mathematical theorem cannot entail its pre-formal truth as evidence-based. It can only identify the explicit/implicit premises that have been used to evidence the, already established, pre-formal truth of a mathematical proposition. Hence visualising and understanding the evidence-based, pre-formal, truth of a mathematical proposition is the only raison d'etre for subsequently seeking a formal proof of the proposition within a formal mathematical language (whether first-order or second order set theory, arithmetic, geometry, etc.) By this yardstick Andrew Wiles' proof of FLT fails to meet the required, evidence-based, criteria for entailing a true arithmetical proposition. -/- Moreover, we offer two scenarios as to why/how Fermat could have laconically concluded in his recorded marginal noting that FLT is a true arithmetical proposition---even though he either did not (or could not to his own satisfaction) succeed in cogently evidencing, and recording, why FLT can be treated as an evidence-based, pre-formal, arithmetical truth (presumably without appeal to properties of real and complex numbers). It is primarily such a putative, unrecorded, evidence-based reasoning underlying Fermat's laconic assertion which this investigation seeks to reconstruct; and to justify by appeal to a plausible resolution of some philosophical ambiguities concerning the relation between evidence-based, pre-formal, truth and formal provability. (shrink)

Andrew Wiles' analytic proof of Fermat's Last Theorem FLT, which appeals to geometrical properties of real and complex numbers, leaves two questions unanswered: (i) What technique might Fermat have used that led him to, even if only briefly, believe he had `a truly marvellous demonstration' of FLT? (ii) Why is x^n+y^n=z^n solvable only for n<3? In this inter-disciplinary perspective, we offer insight into, and answers to, both queries; yielding a pre-formal proof of why FLT can be treated as a true (...) arithmetical proposition (one which, moreover, might not be provable formally in the first-order Peano Arithmetic PA), where we admit only elementary (i.e., number-theoretic) reasoning, without appeal to analytic properties of real and complex numbers. We cogently argue, further, that any formal proof of FLT needs---as is implicitly suggested by Wiles' proof---to appeal essentially to formal geometrical properties of formal arithmetical propositions. (shrink)

Although the Four Colour Theorem is passe, we give an elementary pre-formal proof that transparently illustrates why four colours suffice to chromatically differentiate any set of contiguous, simply connected and bounded, planar spaces; by showing that there is no minimal 4-coloured planar map M. We note that such a pre-formal proof of the Four Colour Theorem highlights the significance of differentiating between: (a) Plato's knowledge as justified true belief, which seeks a formal proof in a first-order mathematical language in order (...) to justify a belief as true; and (b) Piccinini's knowledge as factually grounded belief, which seeks a pre-formal proof, in Pantsar's sense, in order to justify the axioms and rules of inference of a first-order mathematical language which can, then, formally prove the belief as justifiably true under a well-defined interpretation of the language. (shrink)

We argue the thesis that if (1) a physical process is mathematically representable by a Cauchy sequence; and (2) we accept that there can be no infinite processes, i.e., nothing corresponding to infinite sequences, in natural phenomena; then (a) in the absence of an extraneous, evidence-based, proof of `closure' which determines the behaviour of the physical process in the limit as corresponding to a `Cauchy' limit; (b) the physical process must tend to a discontinuity (singularity) which has not been reflected (...) in the Cauchy sequence that seeks to describe the behaviour of the physical process. We support our thesis by mathematical models of the putative behaviours of (i) a virus cluster; (ii) an elastic string; and (iii) a Universe that recycles from Big Bang to Ultimate Implosion, in which parity and local time reversal violation, and the existence of `dark energy' in a multiverse, need not violate Einstein's equations and quantum theory. We suggest that the barriers to modelling such processes in a mathematical language that seeks unambiguous communication are illusory; they merely reflect an attempt to ask of the language chosen for such representation more than it is designed to deliver. (shrink)

We show how removing faith-based beliefs in current philosophies of classical and constructive mathematics admits formal, evidence-based, definitions of constructive mathematics; of a constructively well-defined logic of a formal mathematical language; and of a constructively well-defined model of such a language. -/- We argue that, from an evidence-based perspective, classical approaches which follow Hilbert's formal definitions of quantification can be labelled `theistic'; whilst constructive approaches based on Brouwer's philosophy of Intuitionism can be labelled `atheistic'. -/- We then adopt what may (...) be labelled a finitary, evidence-based, `agnostic' perspective and argue that Brouwerian atheism is merely a restricted perspective within the finitary agnostic perspective, whilst Hilbertian theism contradicts the finitary agnostic perspective. -/- We then consider the argument that Tarski's classic definitions permit an intelligence---whether human or mechanistic---to admit finitary, evidence-based, definitions of the satisfaction and truth of the atomic formulas of the first-order Peano Arithmetic PA over the domain N of the natural numbers in two, hitherto unsuspected and essentially different, ways. -/- We show that the two definitions correspond to two distinctly different---not necessarily evidence-based but complementary---assignments of satisfaction and truth to the compound formulas of PA over N. -/- We further show that the PA axioms are true over N, and that the PA rules of inference preserve truth over N, under both the complementary interpretations; and conclude some unsuspected constructive consequences of such complementarity for the foundations of mathematics, logic, philosophy, and the physical sciences. -/- . (shrink)

Public trust in research and its output is essential for a healthy modern society. Although the research enterprise is self- correcting, this self-regulation occasionally needs help. Over the years, research institutions, professional societies, and governments have established several protocols, codes of conduct, norms, and principles to enhance that trust in research institutions, funders, producers, publishers, and products.