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] <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 <[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) - 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.
