First-order logic?also known as predicate logic, quantificational logic, and first-order predicate calculus?is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over non-logical objects, and allows the use of sentences that contain variables, so that rather than propositions such as "Socrates is a man", one can have expressions in the form "there exists x such that x is Socrates and x is a man", where "there exists" is a quantifier, while x is a variable.[1] This distinguishes it from propositional logic, which does not use quantifiers or relations;[2] in this sense, propositional logic is the foundation of first-order logic.
First-order logic is the standard for the formalization of mathematics into axioms, and is studied in the foundations of mathematics. Peano arithmetic and Zermelo?Fraenkel set theory are axiomatizations of number theory and set theory, respectively, into first-order logic. No first-order theory, however, has the strength to uniquely describe a structure with an infinite domain, such as the natural numbers or the real line. Axiom systems that do fully describe these two structures (that is, categorical axiom systems) can be obtained in stronger logics such as second-order logic. (引用終り) 以上
https://en.wikipedia.org/wiki/Categorical_theory Categorical theory Not to be confused with Category theory.
In mathematical logic, a theory is categorical if it has exactly one model (up to isomorphism).[1] Such a theory can be viewed as defining its model, uniquely characterizing its structure.
In first-order logic, only theories with a finite model can be categorical. Higher-order logic contains categorical theories with an infinite model. For example, the second-order Peano axioms are categorical, having a unique model whose domain is the set of natural numbers N.
In model theory, the notion of a categorical theory is refined with respect to cardinality. A theory is κ-categorical (or categorical in κ) if it has exactly one model of cardinality κ up to isomorphism. Morley's categoricity theorem is a theorem of Michael D. Morley (1965) stating that if a first-order theory in a countable language is categorical in some uncountable cardinality, then it is categorical in all uncountable cardinalities.
Contents 1 History and motivation 2 Examples 3 Properties (引用終り) 以上
5 は自然数のもとで、5 を n に代入すると "5・5 = 25" となり、式は真となる。" n・n=25" が5以外の自然数 n で偽となることは関係がない。少なくとも1つの解が存在すれば、存在量化で真となるに十分である
一方、「ある偶数 n について、 n・n=25である」という文は、偶数の解が存在しないため偽となる。また、「ある奇数 n について、 n・n=25である」という文は、5 が奇数であるため真となる。この事実は変数 n が取りうる値の範囲を示す「議論領域（domain of discourse）」が重要であることを示している。 何らかの述語を満たす値だけを議論領域としたい場合、存在量化では論理積を使用すればよい 例として、「ある奇数 n について、 n・n=25である」という文は「ある自然数 n について、 n は奇数であり、かつ n・n=25 である」という文と論理的に同値である。この場合、「かつ」は論理積を表している
（参考） https://ja.wikipedia.org/wiki/%E5%BD%A2%E5%BC%8F%E7%9A%84%E5%86%AA%E7%B4%9A%E6%95%B0 形式的冪級数 形式的冪級数（英: formal power series）とは、（形式的）多項式の一般化であり、多項式が有限個の項しか持たないのに対し、形式的冪級数は項が有限個でなくてもよい。 定義 A を可換とは限らない環とする。A に係数をもち X を変数（不定元）とする（一変数）形式的冪級数 (formal power series) とは、各 ai (i = 0, 1, 2, …) を A の元として、 Σ n=0～∞a nX^n=a0+a1X+a2X^2+・・ の形をしたものである。ある m が存在して n ≧ m のとき an = 0 となるようなものは多項式と見なすことができる。
例 2.2自然数の全体の集合 N は自然な順序により整列順序集合となる． n ∈ N に対し，n = n ∪ {n} である．すべての n ∈ N に対し， n = 0 なら，m = n となる m ∈ N がとれるから，N は極限点を含まない． 一方X = N ∪ {N} として，X 上の二項関係 <X を， <X= {〈x, y〉 ∈ X2 : (x, y ∈ N かつ x<y)または (x ∈ N かつ y = N) }と定義すると， <X は X 上の整列順序となり，N は X での （<X に関する）極限点となっている． (引用終り) 以上
>>659 (引用開始) >>多分、下記のような日本語「二項関係が整礎（せいそ、英: well-founded）であるとは、真の無限降下列をもたないことである」が、ミスリードです >「空集合Φより簡単な集合はない」を公理にしたのが、正則性公理です 1．下記 wikipedia 正則性公理の説明にも、「∀xについて、無限下降列である x∋x1∋x2∋... は存在しない」が出てきますが 繰り返しますが、ダメなのは、「”xn+1 R xn”なる ”countable infinite descending chains”」(>>651)なのです 逆の「x∈x1∈x2∈... 」なる無限列はOKです。勘違いしているサル二匹がいます (引用終り)
補足説明しておこう 1．問題の”無限下降列”では、下記英文 Well-founded relationの ”Equivalently, assuming the axiom of dependent choice, a relation is well-founded if it contains no countable infinite descending chains: that is, there is no infinite sequence x0, x1, x2, ... of elements of X such that xn+1 R xn for every natural number n.” が最も正確な表現なのです 繰り返すが、”there is no infinite sequence x0, x1, x2, ... of elements of X such that xn+1 R xn for every natural number n.”ね 2．ここ、infiniteでなく、有限だと意味が微妙です 例えて言えば、いま目の前に階段があるとする。下りが上りか？ 自分の立ち位置で違う。下から見れば上りで、上から見れば下り つまり、有限なら、一つの階段に対して、どちらの見方もありうる しかし、エンドレスの無限階段なら？ どちらか一つしかあり得ない。エンドレスだから、逆からの見方はできない。無限に上るか、無限に下るかしかないのです 3．日常語の感覚のまま、「無限降下列」を考えて、”どちらの見方もありうる”！ とハマル おサルがいます（＾＾；
（参考） https://en.wikipedia.org/wiki/Well-founded_relation Well-founded relation In mathematics, a binary relation R is called well-founded (or wellfounded) on a class X if every non-empty subset S ⊆ X has a minimal element with respect to R, that is, an element m not related by sRm (for instance, "s is not smaller than m") for any s ∈ S.
Equivalently, assuming the axiom of dependent choice, a relation is well-founded if it contains no countable infinite descending chains: that is, there is no infinite sequence x0, x1, x2, ... of elements of X such that xn+1 R xn for every natural number n.
https://ja.wikipedia.org/wiki/%E6%95%B4%E7%A4%8E%E9%96%A2%E4%BF%82 数学において、二項関係が整礎（せいそ、英: well-founded）であるとは、真の無限降下列をもたないことである。 定義 集合あるいはクラス X 上の二項関係 R が整礎であるとは、X の空でない任意の部分集合 S が R に関する極小元を持つことをいう[1]。 X が集合であるとき、従属選択公理（英語版）（これは選択公理よりも真に弱く可算選択公理よりも真に強い）を仮定すれば、同値な定義として、関係が整礎であることを可算無限降下列が存在しないこととして定められる[3]。つまり、X の元の無限列 x0, x1, x2, ... で、どんな n についても xn+1 R xn となるようなものはとれない。
>>748 補足 (引用開始) 1．問題の”無限下降列”では、下記英文 Well-founded relationの ”Equivalently, assuming the axiom of dependent choice, a relation is well-founded if it contains no countable infinite descending chains: that is, there is no infinite sequence x0, x1, x2, ... of elements of X such that xn+1 R xn for every natural number n.” が最も正確な表現なのです 繰り返すが、”there is no infinite sequence x0, x1, x2, ... of elements of X such that xn+1 R xn for every natural number n.”ね 例えて言えば、いま目の前に階段があるとする。下りが上りか？ 自分の立ち位置で違う。下から見れば上りで、上から見れば下り つまり、有限なら、一つの階段に対して、どちらの見方もありうる しかし、エンドレスの無限階段なら？ どちらか一つしかあり得ない。エンドレスだから、逆からの見方はできない。無限に上るか、無限に下るかしかないのです (引用終り)
現代数学では、”無限”の意味が多様化してしまった 本来は、「限りが無い」＝”無限”だった 英語でも、finite の語源は、下記のように”L.finire = to end(終わる)”だとか。L.finire は、フィナーレ 【(イタリア)finale】も同様でしょう
下記、英語のInfinity wikipedia などを見ると、 Actual infinity（和訳では「実無限」） と ”potential infinity, in which a non-terminating process (such as "add 1 to the previous number") produces a sequence with no last element, and where each individual result is finite and is achieved in a finite number of steps. ” とに分けて説明しています
https://en.wikipedia.org/wiki/Actual_infinity Actual infinity In the philosophy of mathematics, the abstraction of actual infinity involves the acceptance (if the axiom of infinity is included) of infinite entities as given, actual and completed objects. These might include the set of natural numbers, extended real numbers, transfinite numbers, or even an infinite sequence of rational numbers.[1] Actual infinity is to be contrasted with potential infinity, in which a non-terminating process (such as "add 1 to the previous number") produces a sequence with no last element, and where each individual result is finite and is achieved in a finite number of steps. As a result, potential infinity is often formalized using the concept of limit.[2]
https://en.wikipedia.org/wiki/Infinity Infinity History Early Greek Aristotle (350 BC) distinguished potential infinity from actual infinity, which he regarded as impossible due to the various paradoxes it seemed to produce.[9]
Infinity wikipedia に下記の Wiles's proof of Fermat's Last Theorem と Grothendieck universes の関係が書いてあった これ面白いわ（＾＾；
https://en.wikipedia.org/wiki/Infinity Infinity
The mathematical concept of infinity and the manipulation of infinite sets are used everywhere in mathematics, even in areas such as combinatorics that may seem to have nothing to do with them. For example, Wiles's proof of Fermat's Last Theorem implicitly relies on the existence of very large infinite sets[7] for solving a long-standing problem that is stated in terms of elementary arithmetic.
References [7] McLarty, Colin (2010). "What does it take to prove Fermat's Last Theorem? Grothendieck and the logic of number theory". The Bulletin of Symbolic Logic. 16 (3): 359–377. doi:10.2178/bsl/1286284558. https://www.cambridge.org/core/journals/bulletin-of-symbolic-logic/article/what-does-it-take-to-prove-fermats-last-theorem-grothendieck-and-the-logic-of-number-theory/80EDFF3616F8D58590EBA0DCB9FD2E3E （PDF） https://www.cambridge.org/core/services/aop-cambridge-core/content/view/80EDFF3616F8D58590EBA0DCB9FD2E3E/S1079898600000810a.pdf/what-does-it-take-to-prove-fermats-last-theorem-grothendieck-and-the-logic-of-number-theory.pdf
Abstract. This paper explores the set theoretic assumptions used in the current published proof of Fermat’s Last Theorem, how these assumptions figure in the methods Wiles uses, and the currently known prospects for a proof using weaker assumptions.
Does the proof of Fermat’s Last Theorem (FLT) go beyond Zermelo Fraenkel set theory (ZFC)? Or does it merely use Peano Arithmetic (PA) or some weaker fragment of that? The answers depend on what is meant by “proof” and “use,” and are not entirely known. This paper surveys the current state of these questions and briefly sketches the methods of cohomological number theory used in the existing proof.
The existing proof of FLT is Wiles [1995] plus improvements that do not yet change its character. Far from self-contained it has vast prerequisites merely introduced in the 500 pages of [Cornell et al., 1997]. We will say that the assumptions explicitly used in proofs that Wiles cites as steps in his own are “used in fact in the published proof.” It is currently unknown what assumptions are “used in principle” in the sense of being proof-theoretically indispensable to FLT. Certainly much less than ZFC is used in principle, probably nothing beyond PA, and perhaps much less than that.
The oddly contentious issue is universes, often called Grothendieck universes. 1 On ZFC foundations a universe is an uncountable transitive set U such that U, ∈ satisfies the ZFC axioms in the nicest way: it contains the powerset of each of its elements, and for any function from an element of U to U the range is also an element of U. This is much stronger than merely saying U, ∈ satisfies the ZFC axioms. We do not merely say the powerset axiom “every set has a powerset” is true with all quantifiers relativized to U. Rather, we require “for every set x ∈ U, the powerset of x is also in U” where no quantifier in the definition of the powerset of x is relativized to U. (引用終り) 以上
