8:16 AM
5 hours later…
1:24 PM
Please do feel free to say anything you are thinking and wondering about! (And also corrections, since sometimes I say something wrong, especially symbolically.) I hope my vast walls of text do not create the impression that I don't want a two-way conversation.
Although obviously it's your choice, a far greater amount of derailment would be much appreciated. :)
The problem is very bad for Frege's set theory, because it means Frege's set theory is inconsistent. In standard logic, inconsistent systems cannot be used reliably to distinguish between truth and falsity ever, due to the principle of explosion.
Russell sent Frege a letter shortly before Frege was going to publish his book. My recollection (from learning about it--I was not born at the time) is that Frege was very distraught, though he took the criticism graciously. He added a prominent notice of the problem into his book but still published it. The book was still valuable, in that it still illustrated various insights into developing mathematics atop formal logic.
1:54 PM
The problem with Frege's set theory is unrestricted comprehension. That is, given anything you can express about an object, there is a set of all and only those objects for which it is true.
It's not just that it would make it so that, no matter what predicate (or sentence with one free variable) you have, there is a set that does the work of it.
And that one would be able to construct cardinal numbers as sets of all the sets with that cardinality. For example, one would be able to construct the number 3 as the set of all sets of three elements. Then, with some predicate
F
, there would be three object x
for which Fx
is true, if and only if {x | Fx} ∈ 3
.
The approach to constraining the ontology of sets that was popular initially, after Russell published on Russell's paradox (it had actually also been discovered by Zermelo, but Zermelo had not published about it), is not the approach that is popular today.
The approach that was initially popular was type theory, which is not typically regarded as a set theory today, but rather as a form of higher-order logic. In type theory, every set has a type. The type of a set is one greater than the maximum type of any of the set's members. One cannot define a set of all sets that are not members of themselves.
One can define a set of all sets of type less than
k
that are not members of themselves. This is simply the set of all sets of type strictly less than k
, since no set is a member of itself, and the type of this set is k
. (In a type theory, suppose s ∈ s
. Define n
as the type of s
. Since s ∈ s
, n > n
. That's not okay! So s ∉ s
.)
In first-order logic, x is a term. We can say things about it. The way we can do this is to attach it to a predicate.
F
is a predicate. We cannot things about it, not directly. In second-order logic, we have second-order predicates, also called metapredicates, which can be used to say things about predicates. In second or higher order logic, if G is a unary metapredicate, this is a sentence:
In type theory, there is no limit -- at least no finite limit -- on the type of a term. This means that we can regard things that are syntactically well-formed but in a lower-order logic but that are not terms in a lower-order logic as terms in type theory. The restrictions imposed by the type theory determine what syntactic constructs are permitted. In a type theory, a sentence like
x = y
is a term, just of a different type than x
and y
.
2:29 PM
2:40 PM
I can effectively say that
<
is transitive but not reflexive on the real numbers, by only using <
to talk about numbers. I don't need to be able to say things about <
to do this. Suppose, for simplicity, that our universe of discourse is the real numbers. Then I can express "<
is transitive" by saying:
One approach is to use a higher-order logic. Second-order logic is a kind of higher-order logic. Type theory is another kind. The other approach is to use first-order logic but have
<
not be a predicate, but rather to interpret x < y
as an alternate syntax for an atomic sentence in which x
, y
, and <
are all terms. That is, as it is commonly used in mathematics, "<
" is actually a name for an object! This other approach is what is popular today. Set theory facilitates it.
In fact, I have been understating the situation, since this is the approach that has decisively won out (though that is not the same as saying higher order logics are useless or no longer of interest, neither of which is so).
@Zanna So, suppose we are in a higher-order logic and we want to say, "Some (first-order) predicate is reflexive but not transitive." We can do this, because we can quantify over (first-order) predicates and we can have second-order predicates (like "is transitive") that reign over first-order predicates. In second-order logic, we can quantify over first-order predicates but not over second-order predicates.
In third-order logic, we can quantify over first and second order predicates but not third-order predicates, etc. In a higher order logic where there is no limit, we can quantify over predicates of any particular order. Type theories are such higher order logics.
For our second-order "is good" predicate
G
, maybe we have an axiom that says a predicate is good if and only if it is true of exactly one object:
That's a second-order claim. It's stated sloppily, in part because I don't know the usual conventions in languages of second-order logic. The
∀
in ∀F
is intended to quantify over unary first-order predicates, i.e., over unary predicates that take objects are arguments. The ∃!
in ∃!x
is intended to quantify over objects. (The !
is not related to the order of the quantifier; rather, as you may recall, ∃!x
means "there is exists exactly one x
such that...".)
In first-order logic, whether we use set theory or not, we cannot say exactly that, because predicates are not things that, um, exist. I mean, first-order logic does not have, and does not provided a basis for developing, an ontology of predicates. However, we could have a first-order predicate
G
that means "is a good set," and we could express that a set is good if and only if it has only one element.
Since sets are objects that are intended to do the work of unary predicates, this is the set-theoretic claim that corresponds to that second-order claim.
We can express it as follows (I suppose our universe of discourse is sets, for simplicity, and also because that's the most common approach in set theory):
Since
G
is itself now a unary first-order predicate and sets are intended to do the work of unary predicates, it might seem that we could define a set g
of the good sets, i.e., g := {x | Gx}
. We cannot, though, at least not without giving up extremely useful abilities we do not wish to give up, as g
would be too big.
The reason the ability to define a set
g
(as above) would lead to Russell's paradox is probably not yet clear; it has to do with the actual modern set-theoretic approach that is used to avoid Russell's paradox whilst still having a powerful set theory with a rich ontology. But I will say, if you have some existing set s
, then you can define the subset g
of s
consisting of all those elements of s
that are good. That's okay.
2 hours later…
So, that example had people as the universe of discourse, and we are assuming every person has exactly one godmother.
If we take
F
as a unary predicate meaning "is a godmother of Smith," so that Fx
means "x
is a godmother of Smith," then (under the meaning of "good" elucidated above), F is good.
Similarly, the predicate
F'
, meaning "is a godmother of Jones," so that F'x
means "x
is a godmother of Jones," is good.
As far as I know, there is no single word like "good" that is typically used to mean what "good" means in the above example (i.e., to mean "true of exactly one object").
But a binary predicate
E
is said to be functional when, for any x
, there is exactly one y
such that Exy
. That is, E
is said to be functional when:
I should actually be careful. In
Exy
, if we consider the first argument, x
, to be the independent variable, and the second argument, y
, to be the dependent variable (i.e., if we are thinking of the first argument like an input and the second argument like an output) then "E
is functional" means that for each x
there is exactly one y
that satisfies Exy
.
You will notice the conceptual relationship between a binary predicate
HasGodmother
, where HasGodmother(x, y)
means "x
has y
has a godmother" (or y
is a godmother of x
), and the unary function symbol godmother
, where godmother(x)
means "the unique godmother of x
".
If we adopt the convention that we are only permitted to have function symbols that always succeed, then the binary predicate
Godmother
is functional if and only if it is permitted to define godmother
.
If we adopt the convention that we are permitted to have function symbols that may fail (in which case, the terms they produce do not refer to anything, and any atomic sentence that has such a term as one of its arguments is false, due to falsely asserting the existence of a unique thing), then the binary predicate
Godmother
is functional if and only if terms produced by attaching an argument to the function symbol godmother
never fail to refer to an object.
In either case -- that is, whichever convention we adopt as to when function symbols are permitted -- I am going with the convention that, in
HasGodmother(x, y)
, the first argument, x
, is regarded to be the independent variable, and the second argument, y
, is regarded to be the independent variable.
More generally, but following that same convention, we say that an (n + 1)-ary predicate
F
is functional when, for all combinations of x₁
through xₙ
, there is exactly one y
that make the atomic sentence Fx₁x₂…xₙy
true. That is, we can express "F is functional" with the first-order sentence:
I should clarify that, as written, that is not really a first-order sentence, or any sentence at all. But whatever
n
you pick, writing the formula like that for it expresses that F
is a functional (n + 1)
-ary predicate (with the convention that the n
leading arguments are regarded as independent and the single trailing argument is regarded as dependent). Does that make sense?
5:50 PM
If you allow this definition of "functional" to apply when
n = 0
, i.e., to a unary predicate in which no arguments are regarded as independent and the only argument is regarded as independent, then the above "is good" example does actually mean "is functional."
Functional binary predicates are important to mathematics, in that it is possible to use them to represent relationships between dependent and independent variables. For example, consider the parabola consisting of the points that satisfy the equation
y = x²
. Suppose we use a binary predicate S
to mean "has the square." So Sxy
means the result of squaring x
is y
. That is, y = x²
. We might think of S
as this parabola.
Or suppose we use a unary function symbol
s
to mean "the unique square of." Then sx
means x²
, and we can express y = x²
by writing y = sx
. We might think of s
as this parabola. In a more verbose dialect, we could write S(x, y)
instead of Sxy
and s(x)
instead of sx
. Notice that the notion s(x)
coincides with the notation used to talk about the value of a function in mathematics.
You might therefore wonder if the parabola can be regarded to be the binary predicate
S
or the unary function symbol s
. In second (or higher) order logic (including type theory), we can, because we can say things about S
or s
. We can do algebra with it, we can define what it means to multiply it by a constant, for example. We could define a second-order function symbol D
, where Ds
means "the derivative of s
."
However, in first-order logic, which is what is today nearly universally used as the formal foundation for mathematics, predicates don't adequately capture the notion of a mathematical relation (which I generally just call a "relation," though some people use "relation" to mean "predicate of arity > 1") and function symbols don't adequately capture the notion of a mathematical function (which I generally just call a "function").
Instead, just as sets are objects that do (some) of the work of unary predicates, relations are objects that do (some) of the work of predicates of higher arities, and functions are objects that do (some) of the work of function symbols. It turns out that relations and functions can be constructed as sets, so there is no need to have more than one sort of object to do this.
6:22 PM
5 hours later…
11:09 PM
@traducerad I'm not sure. I would guess not, but I really don't know. I also don't think I have a clear picture of a situation where you would want this--if you end up posting a question, you may want to include that. Is the goal for all ioctl calls on a file to block until the lock is released? Also, do you want advisory or mandatory locking?
(You should feel free to ignore those questions, since I don't know the answer to what you're asking. I suspect that, when you find the answer, it will likely not be through me. But if you do give that information, then I'll try to look into it a bit.)
You may want to ask about this in a room where there are more people, such as the Ubuntu general room, so there are more people who might know the answer. Even then, it's somewhat off the beaten path for that room. Anyway, please feel free to ping me about it there, if you'd like to move the conversation there.
« first day (837 days earlier) ← previous day next day → last day (1562 days later) »