[FOM] Standardization of sets, sorts, and free logic
Dustin Wehr
wehr at cs.toronto.edu
Fri Oct 23 15:52:49 EDT 2015
(in response to recent posts by Freek, Anthony, and others)
I surveyed approaches to partial functions / undefinedness a few years ago,
and came to the conclusion that William Farmer pretty much nailed it:
--"A simple type theory with partial functions and subtypes"
http://imps.mcmaster.ca/doc/nbg-star.pdf
--"Mechanizing the Traditional Approach to Partial Functions"
http://imps.mcmaster.ca/doc/mech-trad-approach.pdf
--"A Set Theory with Support for Partial Functions"
http://imps.mcmaster.ca/doc/nbg-star.pdf
--...and more
Judging from the number of publications, I wouldn't be surprised if he's
thought about it more than anyone else.
Essentially, he adds undefinedness and partial functions to the usual
Tarski semantics for FOL, rather than trying to use an existing language
feature like types. "Undefined" is not an object, but rather, much like
"exceptions" in programming languages, a possible result of evaluating a
term under a given structure and object assignment. "Undefined" propagates
through terms, but not through formulas; atomic formulas, with the
exception of a special "is defined" symbol (i.e. down arrow), and possibly
equality, are false if the evaluation of any of their arguments is
undefined. There is more than one reasonable version of "=" (e.g. false if
either side is undefined, vs. true if both sides are undefined, etc), so
there remains the language design task of either picking one of them to be
"=", or letting "=" be ambiguous and determining the intended version from
context/types, etc.
Farmer's approach works well together with other flavours of
error/undefinedness. To continue the analogy with programming languages,
there are:
--Mistakes caught by the parser or type checker. Terms with such mistakes
are not addressed in the model theory.
--(Catchable) exceptions, like array out-of-bounds or division by zero in
most languages. This is the closest to what Farmer introduced.
--Error values, like "undefined" in Javascript. These are already
well-handled by standard FOL; they are simply additional elements of the
universe. The disadvantage for ATP is that definitional extensions might
need to mention them explicitly, even if it's just to specify that they
propagate up terms. Also, you can't treat them specially with equality; if
both sides of an equation evaluate to the same error value, then the
equation must be true.
Dustin
On Thu, Oct 22, 2015 at 12:58 AM, <fom-request at cs.nyu.edu> wrote:
> Send FOM mailing list submissions to
> fom at cs.nyu.edu
>
> To subscribe or unsubscribe via the World Wide Web, visit
> http://www.cs.nyu.edu/mailman/listinfo/fom
> or, via email, send a message with subject or body 'help' to
> fom-request at cs.nyu.edu
>
> You can reach the person managing the list at
> fom-owner at cs.nyu.edu
>
> When replying, please edit your Subject line so it is more specific
> than "Re: Contents of FOM digest..."
>
> Today's Topics:
>
> 1. 634: Fixed Point Minimization 1 (Harvey Friedman)
> 2. Re: Standardization of sets, sorts, and free logic (Freek Wiedijk)
> 3. 635: Fixed Point Minimization 2 (Harvey Friedman)
> 4. Re: Standardization of sets, sorts, and free logic
> (Anthony Coulter)
>
>
> ---------- Forwarded message ----------
> From: Harvey Friedman <hmflogic at gmail.com>
> To: Foundations of Mathematics <fom at cs.nyu.edu>
> Cc:
> Date: Tue, 20 Oct 2015 23:47:37 -0400
> Subject: [FOM] 634: Fixed Point Minimization 1
> THIS POSTING IS SELF CONTAINED
>
> Fixed Point Minimization presented here may look like it is very different
> from all my previous attempts to move to functions, but having worked
> on Concrete Incompleteness virtually nonstop since 1967, I see that
> everything is related to everything else.
>
> Recall that I am trying to move from the previous relation stuff
>
> PROPOSITION A. Every order invariant relation on Q^k has a
> nonnegatively maximal root with S[0,...,n-1]|>n = S[1,...,n]|>n.
>
> to functions for two reasons. One is to get better explicitly Pi01. The
> other is to get better HUGE. And of course hopefully both at once:
> really good explicitly Pi01 corresponding to HUGE.
>
> Well, this now looks like it is happening. Of course, There are now
> many new things that need more rounds of checking.
>
> It looks like things may well be at last stabilizing, with Proposition
> A for relations, and implicitly Pi01, and the below for functions,
> implicitly Pi01, explicitly Pi01, HUGE, and both.
>
> There is one more avenue that I would like to follow, before getting
> immersed in checking/writing. Right now, I am in several dimensions
> and only order. I need to look at sets of nonnegative integers (i.e.,
> one dimension) with addition. This is needed for continued discussions
> with a colleague who senses some possible connections with
> mathematical physics.
>
> FIXED POINT MINIMIZATION 1
> by
> Harvey Friedman
> October 19, 2015
>
> 1. FIXED POINT MINIMIZERS
>
> DEFINITIION 1.1. Q,Z+,N is the set of all rationals, positive
> integers, nonnegative integers, respectively. We use p,q,x,y,z for
> rationals and tuple of rationals, and k,n,m,r,s,t for positive
> integers, unless indicated otherwise.
>
> DEFINITION 1.2. A relation on Q^k is an R containedin Q^2k. Let R be a
> relation on Q^k. R is reflexive if and only if each x R x. .x is
> related to y if and only if x R y.
>
> DEFINITION 1.3. Let R be a relation on Q^k. A fixed point minimizer
> for R is a function f:D^k into D^k, 0 in D containedin Q, where each
> f(x) is the lexicographically least fixed point of f that is related
> to x.
>
> THEOREM 1.1. Let 0 in D containedin Q be well ordered. Every reflexive
> relation on Q^k has a unique fixed point minimizer with domain D^k.
>
> DEFINITION 1.4. Let x,y in Q^k and E containedin Q^k. x,y are order
> equivalent if and only if for all 1 <= i,j <= k, x_i < x_j iff y_i <
> y_j. E is order invariant if and only if for all order equivalent x,y
> in Q^k, x in E iff y in E. R is an order invariant relation on Q^k if
> and only if R is an order invariant subset of Q^2k. E|<=p = E
> intersection {x in Q^k: max(x) <= p}.
>
> DEFINITION 1.5. Let x,y in Q^k. min(1,x) = (min(1,x_1),...,min(1,x_k)).
>
> PROPOSITION 1.1. Every reflexive order invariant relation on Q^k has a
> fixed point minimizer with min(1,f(1,...,k)) = min(1,f(2,...,k+1)).
>
> It is easily seen that Proposition 1.1 is implicitly Pi01 via the
> Goedel Completeness Theorem. The argument for this also shows that the
> fixed point minimization can be taken to have a certain level of
> concreteness.
>
> THEOREM 1.2. (WKL_0). In Proposition 1.1, if the given relation has
> such a fixed point minimizer then it has such a fixed point minimizer
> that is delta-0-2 in the sense of recursion theory.
>
> THEOREM 1.3. Propositions 1.1, 1.2 are provably equivalent to Con(SRP) over
> WKL_0. For fixed k, Propositions 1.1, 1.2 are provable in SRP. For small
> fixed k, Propositions 1.1, 1.2 are independent of ZFC, assuming Con(SRP).
> These
> results hold if we require that f be delta-0-2 in the sense of
> recursion theory.
>
> For this new statement, I expect to be able to make exact calculations
> of the strength for any fixed k. Such exact calculations are
> incomparably more difficult for Proposition A.
>
> SRP is ZFC + {there exists a limit ordinal with the k-stationary Ramsey
> property}_k. SRP+ = ZFC + (forall n)(therexists a limit ordinal with
> the k-stationary Ramsey property).
>
> NOTE: This is the same if we use k-subtle or k-ineffable.
>
> 2. UPPER SHIFT
>
> DEFINITION 2.1. The upper shift, ush:Q^k into Q^k, is defined as
> follows. ush(x) is the result of adding 1 to all nonnegative
> coordinates of x.
>
> PROPOSITION 2.1. Every reflexive order invariant relation on Q^k has a
> fixed point minimizer with f(ush(x)) = ush(f(x)).
>
> Although Proposition 2.1 is implicitly Pi01, there is a problem seeing
> this via the Goedel Completeness Theorem. We can fix this as follows.
>
> PROPOSITION 2.2. Every reflexive order invariant relation on Q^k has a
> fixed point minimizer with f(ush(x)) = ush(f(x)), x in dom(f)|<=k.
>
> THEOREM 2.3. (WKL_0). The following can be seen via the Goedel
> Completeness Theorem. Proposition 2.2 is implicitly Pi01. In
> Proposition 2.2, if the given relation has such a fixed point
> minimizer then it has such a fixed point minimizer that is delta-0-2
> in the sense of recursion theory.
>
> THEOREM 2.4. Propositions 2.1, 2.2 are provably equivalent to Con(SRP) over
> WKL_0. This is also the case for any fixed k that is not tiny. These
> results hold if we require that f be delta-0-2 in the sense of
> recursion theory.
>
> 3. HUGE CARDINALS
>
> DEFINITION 3.1. x in Q^k is non-increasing if and only if x_1 >= ... >=
> x_k.
>
> DEFINITION 3.2. Let R be a relation on Q^k. A fixed point >= minimizer
> for R is an f:D^k into D^k, 0 in D containedin Q, where each f(x), x
> non-increasing, is the lexicographically least fixed point of f that
> is related to x.
>
> THEOREM 3.1. If we restate Propositions 1.1, 1.2, 2.1, 2.2 with fixed
> point >= minimizers instead of fixed point minimizers, then the same
> results hold.
>
> PROPOSITION 3.2. Every reflexive order invariant relation on Q^k has a
> fixed point >= minimizer, where
> ii. f(x+1) = f(x)+1, min(x) >= 0.
> iii. f(x,k+.5) = (x+1,k+.5), (x,0) in dom(f)|<=k-1.
>
> Although Proposition34.2 is implicitly Pi01, there is a problem seeing
> this via the Goedel Completeness Theorem. We can fix this as follows.
>
> PROPOSITION 3.3. Every reflexive order invariant relation on Q^k has a
> fixed point >= minimizer, where
> ii. f(x+1) = f(x)+1, where 0 <= min(x) <= max(x) <= k.
> iii. f(x,k+.5) = (x+1,k+.5), where (x,0) in dom(f)|<=k-1.
>
> THEOREM 3.4. (WKL_0). The following can be seen via the Goedel
> Completeness Theorem. Proposition 3.3 is implicitly Pi01. In
> Proposition 3.3, if the given relation has such a fixed point
> minimizer then it has such a fixed point minimizer that is delta-0-2
> in the sense of recursion theory.
>
> THEOREM 3.5. Propositions .3.2, 3.3 are provably equivalent to
> Con(HUGE) over WKL_0. This holds if we require that f be delta-0-2 in
> the sense of recursion theory.
>
> 4. TEMPLATES
>
> We first consider Proposition 1.1, which takes the form
>
> PROPOSITION 1.1. Every reflexive order invariant relation on Q^k has a
> fixed point minimizer with a condition.
>
> The particular condition is
>
> min(1,f(1,...,k)) = min(1,f(2,...,k+1)).
>
> There are several kinds of templating that we consider.
>
> a. Vector equations where the dimension is the variable k, using min
> and max. Single or finitely many. No nesting of f.
> b. Equations with specific k, using min and max. Single or finitely
> many. No nesting of f.
> c. Vector inequalities where the dimension is the variable k, with no
> min and max. Single or finitely many. No nesting of f.
> d. Inequalities with specific k, with no min and max. Single or
> finitely many. No nesting of f.
> e. Closure of the graph of f under an order theoretic function
> (specific k's). Single or finitely many.
>
> For further developments, we particularly like to use e).
>
> Recall that the order theoretic sets are those definable over (Q,<)
> with constants allowed. By quantifier elimination, these are just
> Boolean combinations of inequalities between variables, with constants
> allowed.
>
> DEFINITION 4.1. Let E containedin Q^k and H:Q^k into Q^k. E is closed
> under H if and only if for all x in E, H(x) in E. We treat functions
> as graphs.
>
> However, our equation
>
> min(1,f(1,...,k)) = min(1,f(2,...,k+1))
>
> is not quite covered by e). Instead, the condition
>
> f(1,...,k) < 1 implies f(1,...,k) = f(2,...,k+1)
>
> can be used to climb the SRP hierarchy, and it is equivalent to
> closure under H:Q^2k into Q^2k where
>
> H(x) = (2,...,k+1,x_k+1,...,x_2k) if (x_1,...,x_k) = (1,...,k) and
> x_k+1,...,x_2k < 1; x otherwise.
>
> Focusing on e) leads to these four Templates.
>
> TEMPLATE A. Let H:Q^2k into Q^2k be definable in (Q,<) - i.e., order
> theoretic. Every reflexive order invariant relation on Q^k has a fixed
> point minimizer closed under H.
>
> TEMPLATE B. Let H:Q^2k into Q^2k be definable in (Q,<) - i.e., order
> theoretic. Every reflexive order invariant relation on Q^k has a fixed
> point >= minimizer closed under H.
>
> TEMPLATE C. Let H:Q^2k into Q^2k be definable in (Q,<,+1). Every
> reflexive order invariant relation on Q^k has a fixed point minimizer
> closed under H.
>
> TEMPLATE D. Let H:Q^2k into Q^2k be definable in (Q,<,+1). Every
> reflexive order invariant relation on Q^k has a fixed point >=
> minimizer closed under H.
>
> We have seen that a variant of Proposition 1.1 falls under Template A.
> We also have variants falling under Template B (see Theorem 3.1). It
> is clear that Proposition 2.1, 2.2 fall under Template C. Propositions
> 3.2, 3.3 fall under Template D.
>
> Thus we have shown that Templates A,B,C climb through at least the SRP
> hierarchy, and Template D climbs through at least the HUGE hierarchy.
>
> CONJECTURE. Every instance of Templates A,B,C is either provable in SRP
> or refutable in RCA_0. If provable in SRP then provable in WKL_0 +
> Con(SRP).
>
> CONJECTURE. Every instance of Template 5.3 is provable in ZFC +
> j:V(kappa + 1) into V(kappa + 1) or refutable in RCA_0.
>
> 5. FINITE FUNCTIONS
>
> DEFINITION 5.1. Let V containedin Q^k. pi(V) is the set of all
> permutations of elements of V.
>
> DEFINITION 5.2. Let R be a relation on Q^k and E containedin Q . An E
> fixed point minimizer for R is a function f:D^k into D^k, 0 in D
> containedin Q^k, where f(x) is the lexicographically least fixed point
> of f that is related to x, provided x in pi(f[E^k]). An E fixed point
> >= minimizer for R is a function f:D^k into D^k, 0 in D containedin
> Q^k, where f(x) is the lexicographically least fixed point of f that
> is related to x, provided x in pi(f[E^k]) is non-increasing.
>
> PROPOSITION 5.1. Every reflexive order invariant relation on Q^k has
> a {0,...,k} finite fixed point minimizer with min(1,f(1,...,k)) =
> min(1,f(2,...,k+1)).
>
> PROPOSITION 5.2. Every reflexive order invariant relation on Q^k has
> a {0,...,k} finite fixed point minimizer whose <=k composites with
> f(ush(x)) = ush(f(x)), max(x) <= k.
>
> There is an obvious a priori upper bound on the size of D. Since the
> statement is purely order theoretic in parameters 1,...,k+1, we can in
> fact a priori upper bound the numerators and denominators used in D.
> Alternatively, we can move the entire statement into the positive
> integers, and use another arithmetic progression instead of 1,...,k+1.
> These considerations put Propositions 4.1, 4.2 in explicitly Pi01 form.
>
> THEOREM 5.3. Propositions 5.1, 5.2 are provably equivalent to Con(SRP)
> over EFA.
>
> PROPOSITION 5.4. Every reflexive order invariant relation on Q^k has a
> {0,...,k,k+.5} finite fixed point >= minimizer, where
> ii. f(x+1) = f(x)+1, where 0 <= min(x) <= max(x) <= k.
> iii. f(x,k+.5) = (x+1,k+.5), where (x,0) in dom(f)|<= k-1.
>
> The same considerations put Proposition 5.4 in explicitly Pi01 form.
>
> THEOREM 5.5. Proposition 5.4 is provably equivalent to Con(HUGE) over EFA.
>
> **********************************************************
> My website is at https://u.osu.edu/friedman.8/ and my youtube site is at
> https://www.youtube.com/channel/UCdRdeExwKiWndBl4YOxBTEQ
> This is the 634th in a series of self contained numbered
> postings to FOM covering a wide range of topics in f.o.m. The list of
> previous numbered postings #1-599 can be found at the FOM posting
> http://www.cs.nyu.edu/pipermail/fom/2015-August/018887.html
>
> 600: Removing Deep Pathology 1 8/15/15 10:37PM
> 601: Finite Emulation Theory 1/perfect? 8/22/15 1:17AM
> 602: Removing Deep Pathology 2 8/23/15 6:35PM
> 603: Removing Deep Pathology 3 8/25/15 10:24AM
> 604: Finite Emulation Theory 2 8/26/15 2:54PM
> 605: Integer and Real Functions 8/27/15 1:50PM
> 606: Simple Theory of Types 8/29/15 6:30PM
> 607: Hindman's Theorem 8/30/15 3:58PM
> 608: Integer and Real Functions 2 9/1/15 6:40AM
> 609. Finite Continuation Theory 17 9/315 1:17PM
> 610: Function Continuation Theory 1 9/4/15 3:40PM
> 611: Function Emulation/Continuation Theory 2 9/8/15 12:58AM
> 612: Binary Operation Emulation and Continuation 1 9/7/15 4:35PM
> 613: Optimal Function Theory 1 9/13/15 11:30AM
> 614: Adventures in Formalization 1 9/14/15 1:43PM
> 615: Adventures in Formalization 2 9/14/15 1:44PM
> 616: Adventures in Formalization 3 9/14/15 1:45PM
> 617: Removing Connectives 1 9/115/15 7:47AM
> 618: Adventures in Formalization 4 9/15/15 3:07PM
> 619: Nonstandardism 1 9/17/15 9:57AM
> 620: Nonstandardism 2 9/18/15 2:12AM
> 621: Adventures in Formalization 5 9/18/15 12:54PM
> 622: Adventures in Formalization 6 9/29/15 3:33AM
> 623: Optimal Function Theory 2 9/22/15 12:02AM
> 624: Optimal Function Theory 3 9/22/15 11:18AM
> 625: Optimal Function Theory 4 9/23/15 10:16PM
> 626: Optimal Function Theory 5 9/2515 10:26PM
> 627: Optimal Function Theory 6 9/29/15 2:21AM
> 628: Optimal Function Theory 7 10/2/15 6:23PM
> 629: Boolean Algebra/Simplicity 10/3/15 9:41AM
> 630: Optimal Function Theory 8 10/3/15 6PM
> 631: Order Theoretic Optimization 1 10/1215 12:16AM
> 632: Rigorous Formalization of Mathematics 1 10/13/15 8:12PM
> 633: Constrained Function Theory 1 10/18/15 1AM
>
> Harvey Friedman
>
>
>
> ---------- Forwarded message ----------
> From: Freek Wiedijk <freek at cs.ru.nl>
> To: Foundations of Mathematics <fom at cs.nyu.edu>
> Cc:
> Date: Wed, 21 Oct 2015 10:37:00 +0200
> Subject: Re: [FOM] Standardization of sets, sorts, and free logic
> Dear Anthony,
>
> >But the Standard Library needs a Standard
> >Logic, so "(1+1)/0 = 2/0" and "1/0 + 2 = 2 + 1/0" must
> >each either be provable or not provable.
>
> Isn't there a third possibility: both these statements
> are ill-formed? Or does that fall in your "not provable"
> category? But in that case the negation is not provable
> either.
>
> Freek
>
>
>
> ---------- Forwarded message ----------
> From: Harvey Friedman <hmflogic at gmail.com>
> To: Foundations of Mathematics <fom at cs.nyu.edu>
> Cc:
> Date: Wed, 21 Oct 2015 23:52:58 -0400
> Subject: [FOM] 635: Fixed Point Minimization 2
> We continue from
> http://www.cs.nyu.edu/pipermail/fom/2015-October/019260.html
>
> It is arguably preferable to avoid the lexicographic minimization used
> there in favor of the minimization of max(x).
>
> Of course, the advantage of lexicographic minimization is that it is
> deterministic, whereas minimization of max(x) is not. So it seems
> important to have both versions.
>
> Using minimization instead of lexicographic minimization is going to
> add some MORE LAYERS to be checked.
>
> What i want to do here is to restate all of the definitions. The
> results are the same as before. There are also some small changes.
>
> Note that what we called fixed point minimizers in
> http://www.cs.nyu.edu/pipermail/fom/2015-October/019260.html are now
> called lex fixed point minimizers. We reserve the old expression
> "fixed point minimizers" for these new minimizers that minimize
> max(x).
>
> ##############
>
> We now give the altered definitions incorporating both minimizers and
> lex minimizers. We omit the previous definitions that remain
> unchanged, but still listed here. We also present the Templates taking
> into account both kinds of minimizers. In the interest of brevity, the
> Propositions and Theorems are not listed, as they are unchanged from
> http://www.cs.nyu.edu/pipermail/fom/2015-October/019260.html and now
> cover both kinds of minimizers. Also see that I now use non-decreasing
> instead of non-increasing, which I like better. I had fooled myself
> into thinking that I needed to use non-increasing. Actually, either
> can be used.
>
> DEFINITION 1.3. Let R be a relation on Q^k. A fixed point minimizer
> for R is a function f:D^k into D^k, 0 in D containedin Q, where each
> f(x) is a fixed point of f related to x, where no fixed y of f related
> to x has max(y) < max(x). A lex fixed point minimizer for R is a
> function f:D^k into D^k, 0 in D containedin Q, where each f(x) is the
> lexicographically least fixed point of f related to x.
>
> Accordingly, we restate one of the implicitly Pi01 HUGE cardinal
> statements, and also the explicitly Pi01 HUGE cardinal statement.
>
> DEFINITION 3.1. x in Q^k is non-decreasing if and only if x_1 <= ... <=
> x_k.
>
> DEFINITION 3.2. Let R be a relation on Q^k. A fixed point <= minimizer
> for R is an f:D^k into D^k, 0 in D containedin Q, where each f(x), x
> non-decreasing, is a fixed point of f related to x, where no fixed
> point y of f related to x has max(y) < max(x).
>
> DEFINITION 3.3. Let R be a relation on Q^k. A lex fixed point <=
> minimizer for R is an f:D^k into D^k, 0 in D containedin Q, where each
> f(x), x
> non-decreasing, is the lexicographically least fixed point of f related to
> x.
>
> IMPLICITLY Pi01 HUGE. Every reflexive order invariant relation on Q^k
> has a (lex)
> fixed point <= minimizer, where
> ii. f(x+1) = f(x)+1, min(x) >= 0.
> iii. f(k+.5,x) = (k+.5,x+1), (0,x) in dom(f)|<=k-1.
>
> TEMPLATE A. Let H:Q^2k into Q^2k be definable in (Q,<) - i.e., order
> theoretic. Every reflexive order invariant relation on Q^k has a (lex)
> fixed
> point minimizer closed under H.
>
> TEMPLATE B. Let H:Q^2k into Q^2k be definable in (Q,<) - i.e., order
> theoretic. Every reflexive order invariant relation on Q^k has a (lex)
> fixed
> point <= minimizer closed under H.
>
> TEMPLATE C. Let H:Q^2k into Q^2k be definable in (Q,<,+1). Every
> reflexive order invariant relation on Q^k has a (lex) fixed point minimizer
> closed under H.
>
> TEMPLATE D. Let H:Q^2k into Q^2k be definable in (Q,<,+1). Every
> reflexive order invariant relation on Q^k has a (lex) fixed point <=
> minimizer closed under H.
>
> DEFINITION 5.2. Let R be a relation on Q^k and E containedin Q . An E
> fixed point minimizer for R is a function f:D^k into D^k, 0 in D
> containedin Q^k, where f(x) is a fixed point of f related to x, where
> no fixed point y of f related to x has max(y) < max(x). An E fixed
> point
> <= minimizer for R is a function f:D^k into D^k, 0 in D containedin
> Q^k, where f(x) is a fixed point of f related to x, where no fixed
> point y of f related to x has max(y) < max(x).
>
> DEFINITION 5.3. Let R be a relation on Q^k and E containedin Q. An E
> lex fixed point minimizer for R is a function f:D^k into D^k, 0 in D
> containedin Q^k, where f(x) is the lexicographically least fixed point
> of f related to x, provided x in pi(f[E^k]). An E lex fixed point
> <= minimizer for R is a function f:D^k into D^k, 0 in D containedin
> Q^k, where f(x) is the lexicographically least fixed point of f
> related to x, provided x in pi(f[E^k]) is non-decreasing.
>
> EXPLICITLY Pi01 HUGE. Every reflexive order invariant relation on Q^k has a
> {0,...,k,k+.5} finite (lex) fixed point <= minimizer, where
> i. f(x+1) = f(x)+1, where 0 <= min(x) <= max(x) <= k.
> ii. f(k+.5,x) = (k+.5,x+1), (0,x) in dom(f)|<= k-1.
>
> **********************************************************
> My website is at https://u.osu.edu/friedman.8/ and my youtube site is at
> https://www.youtube.com/channel/UCdRdeExwKiWndBl4YOxBTEQ
> This is the 635th in a series of self contained numbered
> postings to FOM covering a wide range of topics in f.o.m. The list of
> previous numbered postings #1-599 can be found at the FOM posting
> http://www.cs.nyu.edu/pipermail/fom/2015-August/018887.html
>
> 600: Removing Deep Pathology 1 8/15/15 10:37PM
> 601: Finite Emulation Theory 1/perfect? 8/22/15 1:17AM
> 602: Removing Deep Pathology 2 8/23/15 6:35PM
> 603: Removing Deep Pathology 3 8/25/15 10:24AM
> 604: Finite Emulation Theory 2 8/26/15 2:54PM
> 605: Integer and Real Functions 8/27/15 1:50PM
> 606: Simple Theory of Types 8/29/15 6:30PM
> 607: Hindman's Theorem 8/30/15 3:58PM
> 608: Integer and Real Functions 2 9/1/15 6:40AM
> 609. Finite Continuation Theory 17 9/315 1:17PM
> 610: Function Continuation Theory 1 9/4/15 3:40PM
> 611: Function Emulation/Continuation Theory 2 9/8/15 12:58AM
> 612: Binary Operation Emulation and Continuation 1 9/7/15 4:35PM
> 613: Optimal Function Theory 1 9/13/15 11:30AM
> 614: Adventures in Formalization 1 9/14/15 1:43PM
> 615: Adventures in Formalization 2 9/14/15 1:44PM
> 616: Adventures in Formalization 3 9/14/15 1:45PM
> 617: Removing Connectives 1 9/115/15 7:47AM
> 618: Adventures in Formalization 4 9/15/15 3:07PM
> 619: Nonstandardism 1 9/17/15 9:57AM
> 620: Nonstandardism 2 9/18/15 2:12AM
> 621: Adventures in Formalization 5 9/18/15 12:54PM
> 622: Adventures in Formalization 6 9/29/15 3:33AM
> 623: Optimal Function Theory 2 9/22/15 12:02AM
> 624: Optimal Function Theory 3 9/22/15 11:18AM
> 625: Optimal Function Theory 4 9/23/15 10:16PM
> 626: Optimal Function Theory 5 9/2515 10:26PM
> 627: Optimal Function Theory 6 9/29/15 2:21AM
> 628: Optimal Function Theory 7 10/2/15 6:23PM
> 629: Boolean Algebra/Simplicity 10/3/15 9:41AM
> 630: Optimal Function Theory 8 10/3/15 6PM
> 631: Order Theoretic Optimization 1 10/1215 12:16AM
> 632: Rigorous Formalization of Mathematics 1 10/13/15 8:12PM
> 633: Constrained Function Theory 1 10/18/15 1AM
> 634: Fixed Point Minimization 1 10/20/15 11:47PM
>
> Harvey Friedman
>
>
>
> ---------- Forwarded message ----------
> From: Anthony Coulter <fom at anthonycoulter.name>
> To: fom at cs.nyu.edu
> Cc:
> Date: Wed, 21 Oct 2015 23:40:33 -0400
> Subject: Re: [FOM] Standardization of sets, sorts, and free logic
> Dear Freek,
>
> > > But the Standard Library needs a Standard
> > > Logic, so "(1+1)/0 = 2/0" and "1/0 + 2 = 2 + 1/0" must
> > > each either be provable or not provable.
>
> > Isn't there a third possibility: both these statements
> > are ill-formed? Or does that fall in your "not provable"
> > category? But in that case the negation is not provable
> > either.
>
> Ah, yes, that is also a possibility. But I don't think it corresponds
> to regular practice. That is, I don't believe that most mathematicians
> would consider formulas involving division by zero to be ill-formed.
> Consider the following three sentences:
>
> 1) all real x: x != 0 -> x/x = 1
> 2) 0 is real
> 3) 0 != 0 -> 0/0 = 1
>
> If "0/0" is not a well-formed term, then (3) is not a well-formed
> sentence and so is formally meaningless. But I believe most
> mathematicians would accept both the well-formedness *and* the
> correctness of the deduction. If you show those three lines to a
> mathematician down your hall and ask if line (3) is meaningless,
> you'll probably be told that "No, line (3) is right. It doesn't
> matter whether 0/0 = 1 because the antecedent is false."
>
> 4) all real x: 1/(sqrt 3 + sin x + cos x) = 1 / (cos x + sin x + sqrt 3)
> 5) all real x: 1/(sqrt 2 + sin x + cos x) = 1 / (cos x + sin x + sqrt 2)
>
> Sentence (4) is true, but sentence (5) entails division by zero at pi/4.
> Does that mean sentence (5) is not well-formed? I was brought up to
> regard "well-formedness" as a syntactic property, and these two
> sentences are syntactically almost identical!
>
> Meanwhile, think of the sophistication required for a computer to figure
> out that sin(x) + cos(x) > -sqrt(2) for all x; we need both this fact
> and the fact that sqrt(3) > sqrt(2) to show that the denominator in
> sentence (4) is always nonzero. Proving that (4) is well-formed will
> take more effort and ingenuity than proving that (4) is true! That seems
> quite backwards to me.
>
> Regards,
> Anthony
>
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20151023/06a9d728/attachment-0001.html>
More information about the FOM
mailing list