On Tuesday, October 23, 2018 at 11:13:52 AM UTC-5, Bruno Marchal wrote: > > > On 22 Oct 2018, at 19:33, Philip Thrift <[email protected] <javascript:>> > wrote: > > > > On Monday, October 22, 2018 at 8:54:47 AM UTC-5, Bruno Marchal wrote: >> >> >> On 22 Oct 2018, at 14:38, Philip Thrift <[email protected]> wrote: >> >> >> >> On Monday, October 22, 2018 at 6:05:41 AM UTC-5, Bruno Marchal wrote: >>> >>> >>> On 21 Oct 2018, at 13:55, Philip Thrift <[email protected]> wrote: >>> >>> >>> >>> It is generally not considered applying Rorty and or Derrida to >>> mathematical language, but mathematics is a language* too, like English. >>> (or programming languages for that matter). >>> >>> >>> Mathematics is no more a language that physics. They use a mathematical >>> language, but the mathematical language is independent of the choice of a >>> theory (written in that mathematical language). >>> >>> We should always keep in mind the distinction between >>> - a mathematical language (usually defined by some grammar which >>> determine the well formed formula) >>> - a mathematical theory. (A precise choice of some formula) >>> - a model of that mathematical theory (a structure satisfying the axioms >>> of a theory, with truth preserving inference rule). >>> - a relation judged plausible between a model of a mathematical theory >>> and a portion or an aspect of some “reality". >>> >>> Exemple: take arithmetic: >>> - the mathematical language is given by -> f, E, A, “(“, “)”, x, y, z … >>> (logical symbols) with “s”, “0”, “+”, “*” (arithmetical symbols) + the >>> usual formation rule (if X and Y are formula, then X -> Y is a formula, >>> etc.) >>> - an arithmetical theory: here the one by Robinson, with only 7 axioms >>> (chosen formula). >>> >>> 1) 0 ≠ s(x) >>> 2) x ≠ y -> s(x) ≠ s(y) >>> 3) x ≠ 0 -> Ey(x = s(y)) >>> 4) x+0 = x >>> 5) x+s(y) = s(x+y) >>> 6) x*0=0 >>> 7) x*s(y)=(x*y)+x >>> + the inference rule of modus ponens >>> >>> - a model is given by any structure verifying (satisfying) the axioms >>> and truth preserving rule. The standard model is the set N together with >>> the usual addition and multiplication (but there are many models, not all >>> isomorphic to the standard model). >>> >>> >>> >>> Bruno >>> >>> >>> >> Mathematics, both pure and applied (e.g. physics), is a collection of >> paradigm-specific and domain-specific languages (PSLs, DSLs), just like >> programming languages. >> >> >> I disagree. All programming languages are equivalent with respect of >> provability, and more or less equivalent when no induction axioms is added >> (in the first order theory of the total functions from N to N computed). >> >> But the theories all differ a lot. It is natural to measure the power of >> a theory by the magnitude of the set of computable functions that the >> theory can prove to be computable. For example Q (the theory above) proves >> the total-computability of a very small set of functions, Peano arithmetic >> (PA) proves a much larger set. ZF proves a very gigantic set, ZF + kappa >> proves an even greater set. You can guess this using incompleteness. For >> example ZF+kappa proves the arithmetical propositions which assert the >> consistency of ZF, and thus also all there consequences. >> >> I look at the arithmetical reality like an ocean, except that it contains >> infinite water, and infinitely many holes in the bottom. For most all, you >> can explore them, without knowing if they have a bottom or not. In some >> case, you can prove that there is a bottom, but that need a very powerful >> theory (like ZF+kappa). >> >> So the arithmetical is something that you can explore, and a theory, any >> theory, is just a lantern which provides some light in the neighbourhood. >> >> It is important to distinguish the arithmetical reality from any >> languages used to describe it, but it is also important to distinguish it >> from all theories, which are only “bodies” throwing light on something >> mainly unknown. >> >> The mathematical reality has noting to do with languages, except that >> languages are needed if machine/people want to share the results of their >> exploration. >> >> The language is the arm. >> The theory is the arm pointing in a direction >> The reality is the moon. >> >> And this is a metaphor, as, with mechanism, the “moon” is but an object >> in (infinities) of number’s dreams (computation seen from inside, I >> eventually defined this using Gödel numbers). >> >> >> >> >> >> >> For example ,quantum field theory can be expressed in Hilbert-space or >> path-integral dialects. >> http://www.fuw.edu.pl/~kostecki/daniel_ranard_essay.pdf >> >> >> >> Like the notion of universal machine, many different theories and >> languages can be used to formulate QM. >> Like Schrodinger/de Broglie Waves (equation/function), or Heisenger >> Matrix, or Feynman's summation. They are “easily” be shown equivalent (when >> discarding the collapse “hallucination”). >> I guess this has to be the case with the relativistic correction, and it >> is of course an open problem for the unknown unified theory (marrying QM >> and GR). But attempts like String Theory shows this with a vengeance, as >> they are many different formulation, mirroring each other in some ways (the >> M theory). >> >> With mechanism, too, as we can take any first order presentation of a >> Turing universal system. >> >> I would say, and can argue, that when we give a theory in the first order >> logic language, we do not introduce any metaphysics, except the one coming >> from the choice of the theory, but the reasoning will not be influenced by >> the choice. That is not the case for second order logic, which indeed, >> forces a bit of (set) metaphysics in the picture. With mechanism, we don’t >> need higher order in the ontology, and the presence of universal >> number/machine in the ontology will make many metaphysics possible for the >> internal phenomenologies. In particular the physical is reduced to what is >> observable for any universal machine, taking into account the impossibility >> for such machine to localise themselves in any particular computations >> (that changes the math a lot). >> >> The paper looks interesting, but I have not much time. >> >> >> >> >> >> A "deconstruction" of first-order logic gives theories which replace >> infinite models with finite ones: >> https://www.jstor.org/stable/2273942 >> >> >> The first page of that paper is definitely interesting, but quite >> advanced, and it would be prematured to use this here. It might help to >> pursue what I have already done, Locally finite theories seems very >> interesting, and I got that by the “von-neuan-Bernaysisation of the theory: >> transforming a theory into a machine which has that theory’s theorems as >> beliefs. Löbianity is kept in that transformation, which I use in my large >> definition of Löbian machine. But most Lôbian machine will not have locally >> finite conception of reality … >> I certainly need the other pages, but I have not the time to search my >> password for JSTOR. >> It is too much precise with respect on the discussion on metaphysics >> here, I think. >> >> >> A theory of physics expressed with a mathematical language inherits the >> metaphysics of the language (e.g. space and time). >> >> >> A theory of physics inherit a theory of mathematics (space and function >> from that space to R), but there is no metaphysics in the theory when they >> are formulated in first order language, and there is not so much >> metaphysics if the theories are formulated *in* an intuitive model of some >> (rich) first order theory, like set theory, or category theory. >> >> Bruno >> >> >> > > My view follows this line: > > > Type theory is a very general and expressive programming language. > (Martin-Löf) > Mathematical proofs correspond to type-theoretic programs . (Curry-Howard) > Type theory, like (ZF) set theory, can be extended in a corresponding way > (forcing). > > Extending Type Theory with Forcing > [ https://ieeexplore.ieee.org/document/6280458 ] > > Thus: There is a programming language that corresponds to each extension > of set theory. > > The philosophy: > > *Truth is not "out-there" in the world. It is in our writing**. (Rorty: > contingency of language) > > > > > > *+* > *Every writing possesses the metaphysics of presence.* (Derrida: > deconstruction). > > * writing = language (natural, formal, mathematical, programming) > > > > For the mind-body perspective, using types makes sense for the first > person perspective, that I recover in the modal logic S4Grz1, unless you > add the universal type, typing is not typically useful for tackling the non > constructive part of truth to which machine are confronted from their first > person points of view. > > I assume mechanism, and thanks to the Church-Turing thesis, or the > equivalent by Post and Kleene, we can study mathematically what machine can > prove and guess, and experience by themselves. For the experience I use an > idea by Theaetetus, somehow imposed by incompleteness. > > To be honest, I have never been much convinced by Rorty and Derrida. I try > to avoid that type of philosophy. I am not saying that I disagree with all > their assertions, but that they lack rigour in the their treatment. > Unclarity of the metaphysical commitment, etc. > > Bruno > >
Modal logics (such as S4Grz) are not only of interest to modal logician types (!) but also agent programming language theorists: *Reasoning about Epistemic States of Agents by Modal Logic Programming* Linh Anh Nguyen https://www.mimuw.edu.pl/~nguyen/nguyen05clima.pdf Abstract. *Modal logic programming is one of appropriate approaches to deal with reasoning about epistemic states of agents. We specify here the least model semantics, the fixpoint semantics, and an SLD-resolution calculus for modal logic programs in the multimodal logic KD4Ig5a, which is intended for reasoning about belief and common belief of agents. We prove that the presented SLD-resolution calculus is sound and complete. We also present a formalization of the wise men puzzle using a modal logic program in KD4Ig5a. This shows that it is worth to study modal logic programming for multi-agent systems.* cf. *S4Grz* in http://sartemov.ws.gc.cuny.edu/files/2012/10/Artemov-Beklemishev.-Provability-logic.pdf and also into type theory *Fibrational Modal Type Theory* https://www.sciencedirect.com/science/article/pii/S1571066116300378 "modalities tend to be mostly studied within classical logic, not within type theory. But modalities should be very useful in type theory" It's programming language theory (PLT) that combines modal logic and type theory. Over the current agent programming languages (like ones based on S4Grz) I proposed the further development of *experiential modal logic*. But its computing substrate (Σ in PLTOS) is the issue. - pt -- You received this message because you are subscribed to the Google Groups "Everything List" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To post to this group, send email to [email protected]. Visit this group at https://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/d/optout.
