@EliahKagan r might be a member of itself

if so, it would be in the wrong set, because all the sets in r are not members of themselves

but if not, it would have to be in r because all sets that are not members of themselves are in r

argh :)

sorry for my absence

it was not due to the horror of a set of all sets that are not members of themselves

@Zanna or rather, r must be a member of itself but it can't be a member of itself. Disaster!

@Zanna Right, r is the set of all sets that are not members of themselves, so it's a member of itself if and only if it isn't:

r ∈ r ↔ r ∉ r

how bad is this problem?

Frege's set theory is inconsistent.

More broadly, any set theory in which the argument in Russell's paradox applies is inconsistent.

Are you asking why a system that falls prey to Russell's paradox is inconsistent, or are you asking how bad it is for a system to be inconsistent?

I guess I'm asking what happened after that hahaha

Do you mean historically?

originally I typed, what happened next historically

but I thought you might be going in another direction and I didn't want to derail

Please derail freely! :)

hahaha ok :)

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.

But Frege's set theory is untenable and must not be used (if one wishes to distinguish truth from falsity).

there are a lot of things in philosophy that have been very useful by being wrong

Indeed.

Though I am interested in what you are thinking of, other than this, if you wish to say.

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.

The fix is to limiting what sets we have.

There is more than one way to do this.

But first it's useful to consider the intended benefit of unrestricted comprehension.

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.

Or, in any case, that does not intuitively capture everything that was appealing about it.

It means that one would be able to have, and use, enormous sets.

Like the set of everything:

{x | x = x}

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.

@EliahKagan I don't think I was thinking of anything specific, only that we are usually making some kind of progress by thinking along some line or another, then someone (possibly the first thinker) comes up with a counterargument, and then you get a better thought

@EliahKagan (One might say that in this construction, 3 would be "the set of all the threes.")

@Zanna Yes.

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.

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

I should say that, like set theory, type theory is not a specific theory. Rather, there are various set theories and various type theories.

"type" does not seem to be a helpful name for this

One can think of the types as objects, predicates, metapredicates, metametapredicates, metametametapredicates, and so forth.

:)

I have been making notes while re-reading here

that is very helpful to me

@Zanna Which thing? The objects, predicates, etc. characterization?

I don't know what you are asking about, sorry!

Sorry, clarified.

sorry, I meant that making notes is very helpful to me

Ah, excellent!

I don't know about these types

I haven't understood that yet

Ah.

but I was amused that the metaness of the predicates kept growing

it's good that we can ask about Ask Ubuntu Meta on Ask Ubuntu Meta

So, consider the atomic sentence:

Fx

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:

GF

The types are discernible syntactically.

@EliahKagan like, this concept we have, F, is a good one

Can you elaborate?

I mean, is that a possible meaning of GF?

Oh. Yes!

I mean, you would probably want to have axioms that elucidate what it means, or what the implications are, of a predicate being good.

But yes.

I just wanted to check that I had got the right idea about it

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.

Unfortunately, I do not know type theory. I have read some parts of Principia Mathematica by Russell and Whitehead, which uses a type theory to develop mathematics, to avoid the problem of Russell's paradox.

@EliahKagan I can see that "good" is a very vague thing. But I realise that I don't have any clear idea of what people actually use this kind of tool for!

Oh.

Suppose one wishes to say, "Some binary relation is transitive but not reflexive."

ok

this kind of thing is familiar

from teaching English as a foreign language

Can you elaborate?

I mean about transitivity.

Are you talking about transitive and reflexive verbs?

If so, I think reflexive verbs are reflexive in a sense that are close to the meaning of reflexivity in logic and mathematics. But I don't think transitive verbs are transitive in a sense that is close to the meaning of transitivity in logic and mathematics.

I meant that we are always talking about what kind of things a particular word or expression or type of word or expression can do and there is a special language for that. A meta language for English

Ah.

@EliahKagan For example, < on real numbers is transitive but not reflexive. If x < y and y < z then x < z. But it is not so that x < x.

(< is also not symmetric: from x < y we cannot conclude that y < x.)

I see that it is helpful to be able to talk about the meaning or action of some thing like > in order to explain how it works

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:

∀x ∀y ∀z ((x < y ∧ y < z) → x < z)

And I can express "< is reflexive" by saying:

∀x (x < x)

Since < is not reflexive, that sentence is false, but it is a well-formed sentence.

So I can express "< is transitive but not reflexive" by saying:

(∀x ∀y ∀z ((x < y ∧ y < z) → x < z)) ∧ ¬ ∀x (x < x)

However, this does not enable me to express, "Some binary relation is transitive but not reflexive."

In first-order logic, I cannot quantify over predicates.

There are two approaches to escape this limitation.

(I am going afk for some time and will hopefully return later)

Okay.

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.

Another example of a second-order claim is, "Something is true of exactly twelve objects."

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:

∀F (GF ↔ ∃!x Fx)

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):

∀y (Gy ↔ ∃!x (x ∈ y))

In practice we are more likely to say it this way:

∀y (Gy ↔ |y| = 1)

(Where |y| means "the cardinality of y", that is, the number of elements in y.)

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.

@EliahKagan yes, your example had exactly one godmother I think

I take it you're referring to that?

yes

These are related but different ideas because godmother in that example was a function symbol.

So, that example had people as the universe of discourse, and we are assuming every person has exactly one godmother.

Consider Smith, who is a person.

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.

And the predicate F'', meaning "is a godmother of Patricia," is good.

But the more interesting property connected to this pertains to binary predicates.

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:

∀x ∃!y Exy

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.

I have seen it done the other way too.

Whichever convention one adopts, "is functional" (as applied to first-order predicates) is a second-order predicate.

this reminds me of when we were talking about arithmetic operations

Go on...

Regarding arithmetic operations, I mean.

from this part here

How does this remind you of that?

(I'm not saying they aren't related.)

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.

@EliahKagan I meant to say, where `HasGodmother(x, y) means "x has y as a godmother".

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:

∀x₁ ∀x₂ … ∀xₙ ∃!y Fx₁x₂…xₙy

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?

Less formally, we say, "y is a function of x₁, x₂, ..., xₙ."

@EliahKagan I am not sure, but I am too sleepy to read properly, so I will resume some time later :(

In that usage, "is a function of" has the same meaning as it has when one says, "position is a function of time."

@EliahKagan I would love this conversation to be less one-sided and for me to have many much more useful things to say

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."

And if you permit nullary function symbols--function symbols of arity 0--then the above relationship between (n + 1)-ary predicates and n-ary function symbols applies to the case of a unary predicate and a nullary function symbol.

@Zanna Is that because what I am saying does not really make sense, or for some other reason?

No, it makes sense!

I mean I wish I had lots of useful things to contribute

Instead of you doing all the work

Only I'm a beginner in this subject

So I have to think a lot

And then I have to spend a lot of time running after elusive documents

@Zanna I don't think I'm doing all the work. I'm typing more than you are, that's true. But I think you may be spending significantly more time on this than I am, reading and thinking about and--as you mentioned recently--taking notes on, it.

:)

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.

For example, a binary relation R is nearly always constructed as its graph, i.e., as the set of ordered pairs (x, y) for which x is related to y under R (i.e., for which xRy is true).

I want to ask you if that makes sense and your thoughts on it...

@Zanna ...but I understand this may be another day.

@EliahKagan * notice that the notation s(x)

@EliahKagan Then xRy is taken to mean (x, y) ∈ R.

Is it possible to lock a file accross mutliple processes using fcntl against ioctl?

you can lock against reads and writes, but what about ioctl?

@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.