gusl: (Default)
In a philosophical conversation with [ profile] spoonless today, I expressed my view succinctly:

"To me, the purpose of axioms should be to discover truths about mathematics, not to make truths."

If the Goldbach conjecture is false, all good axiom systems will agree about this. (You can replace "Goldbach conjecture" with any statement about the integers)

The situation is not the same for infinitary questions. The truth of statements like the Continuum Hypothesis, the determinacy of infinite games, etc is axiom-dependent. Therefore, these statements don't have an objective truth-value. Their meaning is thus relative to a model.


I found someone talking about the phenomenon of axioms making truths:
"Their existence is axiomatic" -Robert Alain, about the non-standard integers

Such fictional objects are useful to the extent that they can give us information about the real objects.

Of course, even standard real analysis deals with non-real objects (the real real numbers are the computable real numbers, which form a countable set). Theorems in real analysis are useful because they tell us something about the computable real numbers.
gusl: (Default)
What are the axioms of the "semantic" turnstile |=?

In the spirit of Locus Solum, I want the freedom to define my symbols to mean anything I want. I like using semantic turnstiles as shorthand for "has property": if I want to say that a class of things has property phi, I will turn it into a class of models (see the second half of this post).

I want the freedom to define my own turnstiles (i.e. my own interpretations), even if that makes model-checking undecidable (e.g. let M |= phi iff phi is true of the output of Turing Machine M). But still, I want the symbol |= to carry some meaning.

The basic syntax I define is:

And as syntactic sugar:

(because it looks dumb to write {M} |= phi)

Axiom 1: definition of what it means for phi to hold in a set of models
M |= phi and N |= phi <=> {M, N} |= phi

|= phi conventionally means that phi is true of every model, i.e. "universal set |= phi", rather than "empty set |= phi". I would like to banish this abuse of notation, by requiring the use of a symbol like "U" for universal set.

Axiom 2: definition of what |/= means
S |/= phi means not S |= phi.

Since I (and all working mathematicians) believe in excluded middle (and non-contradiction), this means that forall S and phi, either S |= phi or S |/= phi, but not both.

As I mentioned earlier, some of the things I like to do with semantic turnstiles might be considered abuse, e.g. introducing mathematical symbols that can't readily be interpreted without importing a theory (which is left implicit in my treatment).

Does this objection apply to my example:

forall n ( exists f_n ( Gaussian |= ( E(X^n) = f_n ( E(X^2) , E(X) ) ) ) ?

The symbols n and f_n are going to disappear before the |= gets interpreted, so this is no problem. On the other hand, the "=" does not disappear. By using "=", I am a assuming a theory of real numbers in which we have equality. I guess this is ok as long as everyone agrees about when the equality holds. To be strict, I might need to plug-in an "implementation" of equality if I am going to say that I have a logic here.

Maybe this is a design issue, though: I can define a model (i.e. probability distribution) as a sequence of moments and deal with them as such. (Since all my queries are about moments, this representation is enough). So instead of E(X^2), we define a (parametric) property of the models, nth-moment(2). In order to check for equality, the model-checker would take the real numbers in some normal form, so it's not so easy afterall...

...or I can bring math into my logic, and define models as real probability distributions. If I do this, things get worse: the model-checker needs to know calculus in order to compute E(X^n).

But why should I need an implementation of equality? I'm just trying to express a definition: Gaussians are defined by first two moments, so it's no surprise that the first two moments uniquely determine the distribution.

[ profile] ekorber says that it's ok to mess around with "|=" even if I don't have everything strictly defined, because mathematicians do sloppy things with it all the time.
gusl: (Default)
Giovanni Sambin is one of the most interesting logicians I know. His "basic logic" seems to be a minimalist idea, embodying only the principle of reflection/variable-substitution, from which he unifies (all?) other logics.

I like this:
One of my principles is that one should study the mind and its products, including mathematics, just as natural scientists study nature.
So with no skyhooks (in the sense of D. Dennett): everything can, and should, be explained virtually from the bottom, that is basing only on the laws of biology.

He calls his philosophy "dynamic constructivism". Reading the paper, it almost sounds like a Buddhist philosophy (all this talk of being attached to Platonism, static foundations, suffering, etc.). I wonder what Henk Barendregt would think.


On the same theme of unifying/formalizing philosophies of mathematics, Ed Zalta is speaking in Amsterdam next month. One year too late for me.
gusl: (Default)
I'm kinda proud of my wiki page on semantics (which is really a pretty stubby index to other wiki pages on all kinds of semantics), especially my mathematical definition.

I find it strange that Wikipedia has no article called Model_(logic). It makes no sense for them have an article on model theory if they don't define "model". Also, correct me if I'm wrong, but saying that model theory is about the "representation of mathematical concepts in terms of set theory" is total BS.

As important as it is to study the representation of mathematical concepts, I don't think it's a well-defined area of study/research, and if it were, it should be called "formalization studies" or (imagining a good future) "mathematical knowledge representation". Also, you can construct mathematical objects with whatever foundation you want. Why do so many people have a fetish for set theory?


UPDATE: Who the hell wrote that the semantics of I-F logic is in terms of "zero-sum games"? These are win-lose games! Sigh... Wikipedia...

Answer: a troll, of course.
gusl: (Default)
From a comment I just wrote to [ profile] jcreed.

Another thing I asked Pfenning about was the proper interpretation of sentences in Linear Logics (it might as well have been about non-monotonic logics, or para-consistent logics (thanks to [ profile] quale for the reminder)). My inclination would be to say that these are "logics" only in the mathematical sense, not in the philosophical sense (i.e. In what I call "philosophical logics", sentences are about real truth. In particular, excluded middle and monotonicity hold.). But when we talk about agents' beliefs, we are in an intensional context, and these two no longer need to hold.

If we claim that sentences of such logics are meaningful, then we should be able to translate them into sentences in philosophical logics, e.g. temporal logics, by jumping out of the agent, and into an outsider's "objective perspective". But I don't see anyone bothering to do this.

For an illustration of what I mean:

While non-monotonic logic can model an agent's belief revision, we know that sentences in this logic are not to be judged as modeling truth. When we see a pair of sentences like:
X |- Z
X, Y |/- Z

we know that |- can't possibly refer to truth (afterall, truth is monotonic). Instead, |- must refer to the agent's beliefs and reasoning processes. Furthermore, this formalism is vague about what refers to the agent's beliefs about facts, what refers to the agent's beliefs about what inferences are valid, or whether the agent's inferences follow this logic blindly, without reflection.

Therefore, if we want to use a true philosophical logic, we should write something like:
B( B(X) ||- B(Z) ) (agent believes that: belief in X, in the default case, justifies belief in Z)

B( B(X) /\ B(Y) ||/- B(Z) ) (agent believes that: belief in X, when accompanied by belief in Y, in the default case, does not justify belief in Z)

Real reasoning involves reflection. Logicians often don't care enough about reflection.
gusl: (Default)
I'm normally not very interested in controversies about foundational axioms for mathematics, since they tend to concern infinities that are too abstract to mean anything to me. Would any scientists care if ZF were all they could work with?
Furthermore, I'm not a Platonist, and I don't like to talk about things in mathematics as being "true" (long ago, I added another argument to this predicate: "theory T is true" became "theory T is good model of domain D", whether D can refer to things in the physical world or to intuitions).

But yesterday, my boss, who is not an academic, let alone a logician, led me to the following insight: in a certain sense, CH is *true*. The independence result implies that one cannot construct a set S such that |Naturals| < |S| < |Reals| (if you could, this would be a proof that ~CH follows from ZFC. I wish I understood how to define this constructibility in terms of axioms).

Any sets that you stick in there are "made up" and cannot be exhibited concretely (not that the Reals is very concrete either, but adding the limits of all Cauchy sequences seems like a rather natural way to construct it).

My boss was thinking about the problem in concrete terms, something which I hadn't done in a long time.
gusl: (Default)
"claim" (How do you say "claim" in Coq?, i.e. an unproven starting point, usually used as a more readable compromise between forward- and backward-chaining) is analogous to a "macro let" (i.e. a 'let' that doesn't evaluate the init-values, but simply binds the declared symbols to code... what's the correct name for it?). In this analogy, a normal 'let' is a claim + proof (proof is evaluation).

Cut-elimination is analogous to macro-expanding this code: it's a way of getting a normal form for the proof/program (which may be interesting if you are interested in coding standards or in automatic programming). But it's a pretty stupid thing to do if you care about program-efficiency / proof-readability, since regular "let" stores the value of the computation (like memoizing), whereas "macro let" doesn't, and will compute the same value several times.
gusl: (Default)
Has anyone ever proven a mathematical result by stating that there must exist a proof of it, and proceeding to prove this non-constructively?
i.e., you prove non-constructively that there exists a proof of A.

I've used arguments that there must exist a proof of A because A is dual to A' (in the sense that the axioms are preserved under permutation of, e.g. union and intersection), for which we already have a proof.
But in this case, it's pretty easy to construct the proof of A by applying a transformation on the proof of A'.
gusl: (Default)
It's impossible to prove Pi_1 statements without axioms that talk about infinity.

If it were possible, I would like to do it right now with Lisp. I have implemented a refuter for general Pi_1 statements, but even though implementing a verifier would never be successful, I still firmly believe in some proofs of Pi_1 statements. That means that I must implicitly accept axioms about infinity, much as I'd like not to.

Here's a nice theorem:
;;;All numbers with an odd number of divisors are perfect squares:
(forall #'(lambda (n) (implies (not (perfect-square-p n)) (evenp (n-divisors n)))))

And here's a nice proof:

(Lemma 1) Forall n in N, n is a perfect square IFF its prime factorization has an even power at all the primes.
(Lemma 2) Forall n in N, n-divisors(n) = PRODUCT (power(p_i,n) + 1) for each prime p_i in the factorization of n

Suppose n is not a perfect square (1)
Then there is a prime p in the prime factorization of n such that its power is odd. (by 1, L1)(2)
Since power(p,n) is odd, then power(p,n) + 1 is even. (3)
Then n-divisors(n) is even. (by 3, L2) (4)

But which axioms am I using in this proof? Are they too hard to dig out of the lemmas? My justification for the lemmas is my visual intuitions. Somewhere in proving them in any kind of system, you would need an axiom about infinity, right?

in case you want the rest of the Lisp code:
Read more... )


gusl: (Default)

December 2016

18 192021222324


RSS Atom

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags