We systematically study several principles and give a principle which is weaker than disjunctive Markov’s principle. We also show that the principle is underivable and strictly weaker than MP∨ in certain extensions of the system EL of elementary analysis.

We show that the so-called weak Markov's principle which states that every pseudo-positive real number is positive is underivable in [MATHEMATICAL SCRIPT CAPITAL T]ω ≔ E-HAω + AC. Since [MATHEMATICAL SCRIPT CAPITAL T]ω allows one to formalize Bishop's constructive mathematics, this makes it unlikely that WMP can be proved within the framework of Bishop-style mathematics . The underivability even holds if the ine.ective schema of full comprehension for negated formulas is added, which allows one to derive the law (...) of excluded middle for such formulas. (shrink)

In 1957, Gödel proved that completeness for intuitionistic predicate logic HPL implies forms of Markov's Principle, MP. The result first appeared, with Kreisel's refinements and elaborations, in Kreisel. Featuring large in the Gödel-Kreisel proofs are applications of the axiom of dependent choice, DC. Also in play is a form of Herbrand's Theorem, one allowing a reduction of HPL derivations for negated prenex formulae to derivations of negations of conjunctions of suitable instances. First, we here show how to deduce (...) Gödel's results by alternative means, ones arguably more elementary than those of Kreisel. We avoid DC and Herbrand's Theorem by marshalling simple facts about negative translations and Markov's Rule. Second, the theorems of Gödel and Kreisel are commonly interpreted as demonstrating the unprovability of completeness for HPL, if means of proof are confined within strictly intuitionistic metamathematics. In the closing section, we assay some doubts about such interpretations. (shrink)

We consider HA*, that is Heyting's Arithmetic extended with transfinite induction over all recursive well orderings, which may be viewed as defining constructive truth, since PA* agrees with classical truth. We prove that Markov's Principle, as a schema, is not provable in HA*, but that HA* is closed under Markov's Rule.

We examine, from a constructive perspective, the relation between the complements of S, T, and S ∩ T in X, where X is either a metric space or a normed linear space. The fundamental question addressed is: If x is distinct from each element of S ∩ T, if s ϵ S, and if t ϵ T, is x distinct from s or from t? Although the classical answer to this question is trivially affirmative, constructive answers involve Markov's (...) class='Hi'>principle and the completeness of metric spaces. (shrink)

It is well known that in Bishop-style constructive mathematics, the closure of the union of two subsets of ℝ is ‘not’ the union of their closures. The dual situation, involving the complement of the closure of the union, is investigated constructively, using completeness of the ambient space in order to avoid any application of Markov's Principle.

Nancy Cartwright believes that we live in a Dappled World– a world in which theories, principles, and methods applicable in one domain may be inapplicable in others; in which there are no universal principles. One of the targets of Cartwright’s arguments for this conclusion is the Causal Markov condition, a condition which has been proposed as a universal condition on causal structures.1 The Causal Markov condition, Cartwright argues, is applicable only in a limited domain of special cases, and thus cannot (...) be used as a universal principle in causal discovery. I have no dispute with any of these claims here. Rather, I wish to argue for a very limited thesis: that the Causal Markov condition is applicable in the specific domain of microscopic quantum mechanical systems; further, that the condition can fruitfully be applied to the much discussed EPR setup. This is perhaps a surprising conclusion, for it is precisely in this domain that Cartwright’s arguments against the Causal Markov condition have been considered to be the most successful. (shrink)

The free energy principle, an influential framework in computational neuroscience and theoretical neurobiology, starts from the assumption that living systems ensure adaptive exchanges with their environment by minimizing the objective function of variational free energy. Following this premise, it claims to deliver a promising integration of the life sciences. In recent work, Markov blankets, one of the central constructs of the free energy principle, have been applied to resolve debates central to philosophy (such as demarcating the boundaries of (...) the mind). The aim of this paper is twofold. First, we trace the development of Markov blankets starting from their standard application in Bayesian networks, via variational inference, to their use in the literature on active inference. We then identify a persistent confusion in the literature between the formal use of Markov blankets as an epistemic tool for Bayesian inference, and their novel metaphysical use in the free energy framework to demarcate the physical boundary between an agent and its environment. Consequently, we propose to distinguish between “Pearl blankets” to refer to the original epistemic use of Markov blankets and “Friston blankets” to refer to the new metaphysical construct. Second, we use this distinction to critically assess claims resting on the application of Markov blankets to philosophical problems. We suggest that this literature would do well in differentiating between two different research programmes: “inference with a model” and “inference within a model.” Only the latter is capable of doing metaphysical work with Markov blankets, but requires additional philosophical premises and cannot be justified by an appeal to the success of the mathematical framework alone. (shrink)

Through the introduction of his ‘common cause principle’ [The Direction of Time, 1956], Hans Reichenbach was the first to formulate a precise link relating causal claims to statements of probability. Despite some criticism, the principle has been hugely influential and successful—a pillar of scientific practice, as well as guiding our reasoning in everyday life. However, Bell’s theorem, taken in conjunction with quantum theory, challenges this principle in a fundamental sense at the microscopic level. For the same reason, (...) the celebrated causal model framework pioneered by Pearl, as well as by Spirtes, Glymour and Scheines, defies satisfactory causal explanations of quantum correlations—the role of the ‘causal Markov condition’ in this framework amounts to a generalisation of Reichenbach’s principle. Much effort has been devoted to the development of quantum causal models to overcome this challenge and to study whether a principled way of causal reasoning, albeit adjusted in its terms, can be maintained when it comes to quantum physics. A clarification of what quantum causal relations are supposed to be is also a much needed step in light of the hotly debated topic of causality in foundations of quantum theory, e.g. in the study of ‘indefinite causal structures’. This paper reports and discusses a framework of quantum causal models and argues that it is promising and interesting for two main reasons. First, it can be seen as a prime example of a recent research programme that took direct and fruitful inspiration from ideas first formulated by Reichenbach—it began by asking, and giving an answer to, how the common cause principle could be generalised appropriately to quantum theoretical terms. Second, the framework did not only facilitate generalisations of the core theorems of the classical framework of causal models, but, above all, it has a theorem at its center that justifies the ‘quantum causal Markov condition’ on the basis of what arguably is a natural definition of causal relations in quantum theory. This provides a conceptually clear grounding of the framework, as well as a proposal for the needed clarification of quantum causal relations in the foundations of quantum theory more generally. (shrink)

The purpose of this paper is an axiomatic study of the interrelations between certain continuity properties. We show that every mapping is sequentially continuous if and only if it is sequentially nondiscontinuous and strongly extensional, and that "every mapping is strongly extensional", "every sequentially nondiscontinuous mapping is sequentially continuous", and a weak version of Markov's principle are equivalent. Also, assuming a consequence of Church's thesis, we prove a version of the Kreisel-Lacombe-Shoenfield-Tsĕitin theorem.

The Common Cause Principle was introduced by HansReichenbach, in The Direction of Time, which was publishedposthumously in 1956. Suppose that two events A and Bare positively correlated: p(A∩B)>p(A)p(B)p(A∩B)>p(A)p(B)p(A\textbackslashcap B)>p(A)p(B). Suppose,moreover, that neither event is a cause of the other. Then,Reichenbach’s Common Cause Principle (RCCP) states that Aand B will have a common cause that renders them conditionallyindependent. Reichenbach incorporated his RCCP into a new probablistictheory of causation, and used it to describe a (purported)macrostatistical temporal asymmetry in analogy with (...) the second law ofthermodynamics. The principle is significant because it posits aconnection between causal structure and probabilistic correlations,thus facilitating causal inference from observed correlations.However, RCCP has been controversial, and a number of counterexampleshave been proposed. RCCP is often seen as an antecedent of theCausal Markov Condition, which plays a central role in causalmodeling and causal inference. RCCP has also been taken to captureassumptions about the behavior of classical systems that appear to beviolated in quantum mechanics. (shrink)

We target the ontological and epistemological ramifications of the proposed distinction between Friston and Pearl blankets. We emphasize the need for empirical testing next to computational modeling. A peculiar aspect of the free energy principle (FEP) is its purported support of radically opposed ontologies of the mind. In our view, the objective ontological aspiration itself should be rejected for a pragmatic instrumentalist view.

Let S be a deductive system such that S-derivability (⊦s) is arithmetic and sound with respect to structures of class K. From simple conditions on K and ⊦s, it follows constructively that the K-completeness of ⊦s implies MP(S), a form of Markov's Principle. If ⊦s is undecidable then MP(S) is independent of first-order Heyting arithmetic. Also, if ⊦s is undecidable and the S proof relation is decidable, then MP(S) is independent of second-order Heyting arithmetic, HAS. Lastly, when ⊦s (...) is many-one complete, MP(S) implies the usual Markov's Principle MP. An immediate corollary is that the Tarski, Beth and Kripke weak completeness theorems for the negative fragment of intuitionistic predicate logic are unobtainable in HAS. Second, each of these: weak completeness for classical predicate logic, weak completeness for the negative fragment of intuitionistic predicate logic and strong completeness for sentential logic implies MP. Beth and Kripke completeness for intuitionistic predicate or sentential logic also entail MP. These results give extensions of the theorem of Gödel and Kreisel (in [4]) that completeness for pure intuitionistic predicate logic requires MP. The assumptions of Godel and Kreisel's original proof included the Axiom of Dependent Choice and Herbrand's Theorem, no use of which is explicit in the present article. (shrink)

It is still a matter of controversy whether the Principle of the Common Cause (PCC) can be used as a basis for sound causal inference. It is thus to be expected that its application to quantum mechanics should be a correspondingly controversial issue. Indeed the early 90’s saw a flurry of papers addressing just this issue in connection with the EPR correlations. Yet, that debate does not seem to have caught up with the most recent literature on causal inference (...) generally, which has moved on to consider the virtues of a generalised PCC-inspired condition, the so-called Causal Markov Condition (CMC). In this paper we argue that the CMC is an appropriate benchmark for debating possible causal explanations of the EPR correlations. But we go on to take issue with some pronouncements on EPR by defenders of the CMC. (shrink)

New epistemic principles are formulated in the language of Shapiro's system of Epistemic Arithmetic. It is argued that some plausibility can be attributed to these principles. The relations between these principles and variants of controversial constructivistic principles are investigated. Special attention is given to variants of the intuitionistic version of Church's thesis and to variants of Markov's principle.

Five recursively axiomatizable theories extending Kleene's intuitionistic theory FIM of numbers and numbertheoretic sequences are introduced and shown to be consistent, by a modified relative realizability interpretation which verifies that every sequence classically defined by a Π11 formula is unavoidable and that no sequence can fail to be classically Δ11. The analytical form of Markov's Principle fails under the interpretation. The notion of strongly inadmissible rule of inference is introduced, with examples.

We investigate which part of Brouwer’s Intuitionistic Mathematics is finitistically justifiable or guaranteed in Hilbert’s Finitism, in the same way as similar investigations on Classical Mathematics (i.e., which part is equiconsistent with$\textbf {PRA}$or consistent provably in$\textbf {PRA}$) already done quite extensively in proof theory and reverse mathematics. While we already knew a contrast from the classical situation concerning the continuity principle, more contrasts turn out: we show that several principles are finitistically justifiable or guaranteed which are classically not. Among (...) them are:(i)fan theorem for decidable fans but arbitrary bars;(ii)continuity principle and the axiom of choice both for arbitrary formulae; and(iii)$\Sigma _2$induction and dependent choice. We also show that Markov’s principle MP does not change this situation; that neither does lesser limited principle of omniscience LLPO (except the choice along functions); but that limited principle of omniscience LPO makes the situation completely classical. (shrink)

The free-energy principle (FEP) builds on an assumption that sensor–motor loops exhibit Markov blankets in stationary state. We argue that there is rarely reason to assume a system's internal and external states are conditionally independent given the sensorimotor states, and often reason to assume otherwise. However, under mild assumptions internal and external states are conditionally independent given the sensorimotor history.

The extended mind thesis claims that a subject’s mind sometimes encompasses the environmental props the subject interacts with while solving cognitive tasks. Recently, the debate over the extended mind has been focused on Markov Blankets: the statistical boundaries separating biological systems from the environment. Here, I argue such a focus is mistaken, because Markov Blankets neither adjudicate, nor help us adjudicate, whether the extended mind thesis is true. To do so, I briefly introduce Markov Blankets and the free energy (...) class='Hi'>principle in Section 2. I then turn from exposition to criticism. In Section 3, I argue that using Markov Blankets to determine whether the mind extends will provide us with an answer based on circular reasoning. In Section 4, I consider whether Markov Blankets help us track the boundaries of the mind, answering in the negative. This is because resorting to Markov Blankets to track the boundaries of the mind yields extensionally inadequate conclusions which violate the parity principle. In Section 5, I further argue that Markov Blankets led us to sidestep the debate over the extended mind, as they make internalism about the mind vacuously true. A brief concluding paragraph follows. (shrink)

We consider the restriction of classical principles like Excluded Middle, Markov’s Principle, König’s Lemma to arithmetical formulas of degree 2. For any such principle, we find simple mathematical statements which are intuitionistically equivalent to it, provided we restrict universal quantifications over maps to computable maps.

The completeness w.r.t. Kripke frames with equality (or, equivalently, w.r.t. Kripke sheaves, [ 8 ] or [4, Sect. 3.6]) is established for three superintuitionistic predicate logics: ( Q - H + D *), ( Q - H + D *&K), ( Q - H + D *& K & J ). Here Q - H is intuitionistic predicate logic, J is the principle of the weak excluded middle, K is Kuroda’s axiom, and D * (cf. [ 12 ]) is (...) a weakened version of the well-known constant domains principle D . Namely, the formula D states that any individual has ancestors in earlier worlds, and D * states that any individual has $${\neg\neg}$$ -ancestors (i.e., ancestors up to $${\neg\neg}$$ -equality) in earlier worlds. In particular, the logic ( Q - H + D *& K & J ) is the Kripke sheaf completion of ( Q - H + E & K & J ), where E is a version of Markov’s principle (cf. [ 12 ]). On the other hand, we show that the logic ( Q - H + D *& J ) is incomplete w.r.t. Kripke sheaves. (shrink)

Realizabilities are powerful tools for establishing consistency and independence results for theories based on intuitionistic logic. Troelstra discovered principles ECT 0 and GC 1 which precisely characterize formal number and function realizability for intuitionistic arithmetic and analysis, respectively. Building on Troelstra's results and using his methods, we introduce the notions of Church domain and domain of continuity in order to demonstrate the optimality of “almost negativity” in ECT 0 and GC 1 ; strengthen “double negation shift” DNS 0 to DNS (...) 1 and use it with GC 1 and Markov's Principle MP to characterize the classically provably realizable formulas of analysis; and show that intuitionistic analysis with GC 1 , MP and DNS 1 is consistent and satisfies Troelstra's and Church's Rules. We end with a discussion of semi-intuitionistic theories and a conjecture. (shrink)

In this note we compare propositional logics for closed substitutions and propositional logics for open substitutions in constructive arithmetical theories. We provide a strong example where these logics diverge in an essential way. We prove that for Markov's Arithmetic, that is, Heyting's Arithmetic plus Markov's principle plus Extended Church's Thesis, the logic of closed and the logic of open substitutions are the same.

Logic has a fundamental role in the philosophy of Franjo Marković (1845-1914). His theory of concepts and reasoning is analyzed, especially with respect to the essential role of the principle of sufficient reason and in connection with the concept of causality. The interplay of various types of evidence in Marković's inductive-deductive logic is analysed by means of contemporary justification logic tools.

There has been much criticism of the idea that Friston's free-energy principle can unite the life and mind sciences. Here, we argue that perhaps the greatest problem for the totalizing ambitions of its proponents is a failure to recognize the importance of evolutionary dynamics and to provide a convincing adaptive story relating free-energy minimization to organismal fitness.

Woodward present an argument for the Causal Markov Condition (CMC) on the basis of a principle they dub ‘modularity’ ([1999, 2004]). I show that the conclusion of their argument is not in fact the CMC but a substantially weaker proposition. In addition, I show that their argument is invalid and trace this invalidity to two features of modularity, namely, that it is stated in terms of pairwise independence and ‘arrow-breaking’ interventions. Hausman & Woodward's argument can be rendered valid through (...) a reformulation of modularity, but it is doubtful that the argument so revised provides any substantially new insight regarding the basis of the CMC. Introduction The CMC versus Hausman & Woodward's conclusion Hausman & Woodward's argument Modularity and independent error terms Conclusion Appendix: D-separation. (shrink)

We call a logic regular for a semantics when the satisfaction predicate for at least one of its nontheorems is closed under double negation. Such intuitionistic theories as second-order Heyting arithmetic HAS and the intuitionistic set theory IZF prove completeness for no regular logics, no matter how simple or complicated. Any extensions of those theories proving completeness for regular logics are classical, i.e., they derive the tertium non datur. When an intuitionistic metatheory features anticlassical principles or recognizes that a logic (...) regular for a semantics is nonclassical, it proves explicitly that the logic is incomplete with respect to that semantics. Logics regular relative to Tarski. Beth and Kripke semantics form a large collection that includes propositional and predicate intuitionistic, intermediate and classical logics. These results are corollaries of a single theorem. A variant of its proof yields a generalization of the Gödel-Kreisel Theorem linking weak completeness for intuitionistic predicate logic to Markov's Principle. (shrink)

I sympathize with Prosen’s conviction in integrating enactivism, the free-energy principle, and the extended-mind hypothesis. However, I show that he uses the concept of “boundary” ambiguously. By disambiguating it, I suggest that we can keep both Markov blankets and operational closure as ways of drawing the boundaries of a cognitive system. Nevertheless, from an enactive perspective, neither of those boundaries is a “cognitive” boundary.

We define a notion of realizability, based on a new assignment of formulas, which does not care for precise witnesses of existential statements, but only for bounds for them. The novel form of realizability supports a very general form of the FAN theorem, refutes Markov's principle but meshes well with some classical principles, including the lesser limited principle of omniscience and weak König's lemma. We discuss some applications, as well as some previous results in the literature.

Twenty-first century science faces a dilemma. Two of its well-verified foundation stones - relativity and quantum theory - have proven inconsistent. Resolution of the conflict has resisted improvements in experimental precision leaving some to believe that some fundamental understanding in our world-view may need modification or even radical reform. Employment of the wave-front model of electrodynamics, as a propagation process with a Markov property, may offer just such a clarification.

The free energy principle is sometimes put forward as accounting for biological self-organization and cognition. It states that for a system to maintain non-equilibrium steady-state with its environment it can be described as minimising its free energy. It is said to be entirely scale-free, applying to anything from particles to organisms, and interactive machines, spanning from the abiotic to the biotic. Because the FEP is so general in its application, one might wonder whether this framework can capture anything specific (...) to biology. We take steps to correct for this here. We first explicate the worry, taking pebbles as examples of an abiotic system, and then discuss to what extent the FEP can distinguish its dynamics from an organism’s. We articulate the notion of ‘autonomy as precarious operational closure’ from the enactive literature, and investigate how it can be unpacked within the FEP. This enables the FEP to delineate between the abiotic and the biotic; avoiding the pebble worry that keeps it out of touch with the living systems we encounter in the world. (shrink)

The idea of obtaining a pilot-wave quantum theory on a lattice with discrete time is presented. The motion of quantum particles is described by a \-distributed Markov chain. Stochastic matrices of the process are found by the discrete version of the least-action principle. Probability currents are the consequence of Hamilton’s principle and the stochasticity of the Markov process is minimized. As an example, stochastic motion of single particles in a double-slit experiment is examined.

We put together several observations on constructive negation. First, Russell anticipated intuitionistic logic by clearly distinguishing propositional principles implying the law of the excluded middle from remaining valid principles. He stated what was later called Peirce’s law. This is important in connection with the method used later by Heyting for developing his axiomatization of intuitionistic logic. Second, a work by Dragalin and his students provides easy embeddings of classical arithmetic and analysis into intuitionistic negationless systems. In the last section, we (...) present in some detail a stepwise construction of negation which essentially concluded the formation of the logical base of the Russian constructivist school. Markov’s own proof of Markov’s principle (different from later proofs by Friedman and Dragalin) is described. (shrink)

It is still a matter of controversy whether the Principle of the Common Cause can be used as a basis for sound causal inference. It is thus to be expected that its application to quantum mechanics should be a correspondingly controversial issue. Indeed the early 90’s saw a flurry of papers addressing just this issue in connection with the EPR correlations. Yet, that debate does not seem to have caught up with the most recent literature on causal inference generally, (...) which has moved on to consider the virtues of a generalised PCC inspired condition, the so called Causal Markov Condition. In this paper we argue that the CMC is an appropriate benchmark for debating possible causal explanations of the EPR correlations. But we go on to take issue with some pronouncements on EPR by defenders of the CMC. (shrink)

In his previous work, the author has introduced the axiom schema of inductive dichotomy, a weak variant of the axiom schema of inductive definition, and used this schema for elementary ) positive operators to separate open and clopen determinacies for those games in which two players make choices from infinitely many alternatives in various circumstances. Among the studies on variants of inductive definitions for bounded ) positive operators, the present article investigates inductive dichotomy for these operators, and applies it to (...) constructive investigations of variants of determinacy statements for those games in which the players make choices from only finitely many alternatives. As a result, three formulations of open determinacy, that are all classically equivalent with each other, are equivalent to three different semi-classical principles, namely Markov’s Principle, Lesser Limited Principle of Omniscience and Limited Principle of Omniscience, over a suitable constructive base theory that proves clopen determinacy. Open and clopen determinacies for these games are thus separated. Some basic results on variants of inductive definitions for \ positive operators will also be given. (shrink)

Beth models of analysis are used in model theoretic proofs of the disjunction and (numerical) existence property. By glueing strings of models one obtains a model that combines the properties of the given models. The method asks for a common generalization of Kripke and Beth models. The proof is carried out in intuitionistic analysis plus Markov's Principle. The main new feature is the external use of intuitionistic principles to prove their own preservation under glueing.

In this paper we give a new proof of the characterization of the closed fragment of the provability logic of Heyting's Arithmetic. We also provide a characterization of the closed fragment of the provability logic of Heyting's Arithmetic plus Markov's Principle and Heyting's Arithmetic plus Primitive Recursive Markov's Principle.

It is shown that—over Bishop's constructive mathematics—the indecomposability of ℝ is equivalent to the statement that all functions from a complete metric space into a metric space are sequentially nondiscontinuous. Furthermore we prove that the indecomposability of ℝ \ {0} is equivalent to the negation of the disjunctive version of Markov's Principle. These results contribute to the programme of Constructive Reverse Mathematics.

F. Richman raised the question of whether the following principle of second order arithmetic is valid in intuitionistic higher order arithmetic $\mathbf{HAH}$: $\forall X\lbrack\forall x(x \in X \vee \neg x \in X) \wedge \forall Y(\forall x(x \in Y \vee \neg x \in Y) \rightarrow \forall x(x \in X \rightarrow x \in Y) \vee \forall x \neg(x \in X \wedge x \in Y)) \rightarrow \exists n\forall x(x \in X \rightarrow x = n)\rbrack$, and if not, whether assuming Church's Thesis CT (...) and Markov's Principle MP would help. Blass and Scedrov gave models of $\mathbf{HAH}$ in which this principle, which we call RP, is not valid, but their models do not satisfy either CT or MP. In this paper a realizability topos Lif is constructed in which CT and MP hold, but RP is false. (It is shown, however, that $RP$ is derivable in $\mathbf{HAH} + \mathrm{CT} + \mathrm{MP} + \mathrm{ECT}_0$, so RP holds in the effective topos.) Lif is a generalization of a realizability notion invented by V. Lifschitz. Furthermore, Lif is a subtopos of the effective topos. (shrink)

The so-called weak König's lemma WKL asserts the existence of an infinite path b in any infinite binary tree . Based on this principle one can formulate subsystems of higher-order arithmetic which allow to carry out very substantial parts of classical mathematics but are Π 2 0 -conservative over primitive recursive arithmetic PRA . In Kohlenbach 1239–1273) we established such conservation results relative to finite type extensions PRA ω of PRA . In this setting one can consider also a (...) uniform version UWKL of WKL which asserts the existence of a functional Φ which selects uniformly in a given infinite binary tree f an infinite path Φf of that tree. This uniform version of WKL is of interest in the context of explicit mathematics as developed by S. Feferman. The elimination process in Kohlenbach [10] actually can be used to eliminate even this uniform weak König's lemma provided that PRA ω only has a quantifier-free rule of extensionality QF-ER instead of the full axioms of extensionality for all finite types. In this paper we show that in the presence of , UWKL is much stronger than WKL: whereas WKL remains to be Π 2 0 -conservative over PRA, PRA ω ++ UWKL contains full Peano arithmetic PA. We also investigate the proof–theoretic as well as the computational strength of UWKL relative to the intuitionistic variant of PRA ω both with and without the Markov principle. (shrink)

Beth models of analysis are used in model theoretic proofs of the disjunction and existence property. By glueing strings of models one obtains a model that combines the properties of the given models. The method asks for a common generalization of Kripke and Beth models. The proof is carried out in intuitionistic analysis plus Markov's Principle. The main new feature is the external use of intuitionistic principles to prove their own preservation under glueing.

Several authors have made claims about the compatibility between the Free Energy Principle and theories of autopoiesis and enaction. Many see these theories as natural partners or as making similar statements about the nature of biological and cognitive systems. We critically examine these claims and identify a series of misreadings and misinterpretations of key enactive concepts. In particular, we notice a tendency to disregard the operational definition of autopoiesis and the distinction between a system’s structure and its organization. Other (...) misreadings concern the conflation of processes of self-distinction in operationally closed systems and Markov blankets. Deeper theoretical tensions underlie some of these misinterpretations. FEP assumes systems that reach a non-equilibrium steady state and are enveloped by a Markov blanket. We argue that these assumptions contradict the historicity of sense-making that is explicit in the enactive approach. Enactive concepts such as adaptivity and agency are defined in terms of the modulation of parameters and constraints of the agent-environment coupling, which entail the possibility of changes in variable and parameter sets, constraints, and in the dynamical laws affecting the system. This allows enaction to address the path-dependent diversity of human bodies and minds. We argue that these ideas are incompatible with the time invariance of non-equilibrium steady states assumed by the FEP. In addition, the enactive perspective foregrounds the enabling and constitutive roles played by the world in sense-making, agency, development. We argue that this view of transactional and constitutive relations between organisms and environments is a challenge to the FEP. Once we move beyond superficial similarities, identify misreadings, and examine the theoretical commitments of the two approaches, we reach the conclusion that far from being easily integrated, the FEP, as it stands formulated today, is in tension with the theories of autopoiesis and enaction. (shrink)

This paper introduces an extension A of Kleene's axiomatization of Brouwer's intuitionistic analysis, in which the classical arithmetical and analytical hierarchies are faithfully represented as hierarchies of the domains of continuity. A domain of continuity is a relation R(α) on Baire space with the property that every constructive partial functional defined on {α : R(α)} is continuous there. The domains of continuity for A coincide with the stable relations (those equivalent in A to their double negations), while every relation R(α) (...) is equivalent in A to ∃αA(α, β) for some stable A(α, β) (which belongs to the classical analytical hierarchy). The logic of A is intuitionistic. The axioms of A include countable comprehension, bar induction, Troelstra's generalized continuous choice, primitive recursive Markov's Principle and a classical axiom of dependent choices proposed by Krauss. Constructive dependent choices, and constructive and classical countable choice, are theorems, A is maximal with respect to classical Kleene function realizability, which establishes its consistency. The usual disjunction and (recursive) existence properties ensure that A preserves the constructive sense of "or" and "there exists.". (shrink)

In this paper I dispute the current view that intuitionistic logic is the common basis for the three main trends of constructivism in the philosophy of mathematics: intuitionism, Russian constructivism and Bishop’s constructivism. The point is that the so-called ‘Markov’s principle’, which is accepted by Russian constructivists and rejected by the other two, is expressible in intuitionistic first-order logic, and so it appears to have the status of a logical principle. The result of appending this principle to (...) a complete intuitionistic axiom system for first-order predicate logic constitutes a new logic, which could well be called ‘Markov’s logic’, and which should be regarded as the true logical system underlying Russian constructivism. (shrink)