> On 22 Oct 2018, at 19:33, Philip Thrift <cloudver...@gmail.com> 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 <cloud...@gmail.com <javascript:>> >> 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 <cloud...@gmail.com <>> 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 >> <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 <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 > > - 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 everything-list+unsubscr...@googlegroups.com > <mailto:everything-list+unsubscr...@googlegroups.com>. > To post to this group, send email to everything-list@googlegroups.com > <mailto:everything-list@googlegroups.com>. > Visit this group at https://groups.google.com/group/everything-list > <https://groups.google.com/group/everything-list>. > For more options, visit https://groups.google.com/d/optout > <https://groups.google.com/d/optout>. -- 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 everything-list+unsubscr...@googlegroups.com. To post to this group, send email to everything-list@googlegroups.com. Visit this group at https://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/d/optout.
