Зачем нужны аксиомы?

спасибо что демонстрируеш , что действительно есть люди не могущие в указатели , не могущие различать имя и именуемое.

пока я вижу только то, что ты не умеешь в русский. Судя по development тредам твоё умение в указатели, это тоже под вопросом ;)

меридианы не есть параллельные прямые.

покажи, что медианы не являются параллельными прямыми, напомню, что наше пространство это поверхность сферы.

деточка когда читаеш фантастику полезно верить ибо кайф

когда книжку закрыл всёж стоит отметить что полученые сведенья худ.лит.

пусть геометрия нашего 3мерия имеет положительную? кривизну - тогда не существует параллельных прямых в нём.

а не «параллельные пересикаются».

ибо семантика фразы «обьект со свойством быть А есть обьект без свойства быть А » очевидна.

а у вас молитвы в голове.

тогда не существует параллельных прямых в нём.

принято.

рад. учёба полезна.

хотя доказательство там простое и разбирается в начале любого учебника по всяким пруф-ассистентам

«Не тривиально» и «не канонично» это там технические термины — то есть не сводится к computional equality и сразу к каноническому конструктору identity type (не знаю, используют ли последний в Coq). Так-то оно «простое»:

open import Data.Nat
open import Relation.Binary.PropositionalEquality

-- | cong/rec
a+0≡a : ∀ a → a + 0 ≡ a
a+0≡a zero = refl
a+0≡a (suc a) = cong suc (a+0≡a a)

-- | cong/rec via induction
a+0≡a′ : ∀ a → a + 0 ≡ a
a+0≡a′ = ind (λ a → a + 0 ≡ a) refl (λ _ → cong suc) where
  ind : (P : ℕ → Set) → P 0 → (∀ a → P a → P (1 + a)) → ∀ a → P a
  ind _ P₀ _ zero = P₀
  ind P P₀ next (suc a) = next a (ind P P₀ next a)

-- | cong/rec
a+1+b≡1+a+b : ∀ a b → a + (1 + b) ≡ 1 + (a + b)
a+1+b≡1+a+b zero _ = refl
a+1+b≡1+a+b (suc a) b = cong suc (a+1+b≡1+a+b a b)

-- | trans/cong/rec
+-comm : ∀ a b → a + b ≡ b + a
+-comm zero b = sym (a+0≡a b)
+-comm (suc a) b = trans (cong suc (+-comm a b)) (sym (a+1+b≡1+a+b b a))

open ≡-Reasoning

-- | trans/cong/rec with equational reasoning
+-comm′ : ∀ a b → a + b ≡ b + a
+-comm′ zero b = sym (a+0≡a b)
+-comm′ (suc a) b = begin
  suc a + b   ≡⟨ refl ⟩ -- can be omitted, so that via β:
  suc (a + b) ≡⟨ cong suc (+-comm′ a b) ⟩
  suc (b + a) ≡⟨ sym (a+1+b≡1+a+b b a) ⟩
  b + suc a   ∎

Созрел вопрос: а зачем вообще нужны математические или иные аксиомы?

Чтобы ответить на этот вопрос, тоже нужно вводить аксиомы. Витгенштейна я уже основательно подзабыл, так что пересказывать не буду.

Возможно ли пользуясь только аксиомами сформулировать, скажем, теорему Пифагора? Не доказать, а именно открыть, сформулировать.

Конкретно теорема Пифагора была открыта до открытия аксиом

А если нет, то какой тогда прок от таких оснований в деле накопления новых знаний?

Можно открывать интуитивно неочевидные теоремы.

а чуть ли не визуально конструируются исходя из жизненного опыта человека и его здравого смысла.

На высоких уровнях знания то и другое сосет с причмоком.

прям как церковь. математика - яд, берегите ребят.

Есть децл. Скорее математика без кормления во время обучения реальными данными, с коллизиями, шумом и артефактами. А то так и останутся в мире сферических поней в вакууме.

лолшто? струны это к физикам, математикам на нее чхать

А физики (экспериментаторы) считают наоборот. Пинают туда-сюда как внебрачного ребенка.

На аксиомах удобно строить теорию. Она ценна сама по себе и универсальна. Еще есть чувственный опыт, который неуниверсален и уникален. И есть т.н. знания кентаврового типа, которые дружат теорию с чувтсвенным опытом. Гугли философию науки.

мир сферических поней в вакууме

как будто чтото плохое.

Релиз Go 1.1 (комментарий)

Можно сменить слово «ЯП» на что-то более широкое, но смысл передан абсолютно точно)

Обычно такие вопросы в 5-м классе задают на первом уроке алгебры.

на что-то более широкое

математика

Не? Есть общепринятая терминология, например — тривиальная группа, не изоморфные тривиальной группе группы (то есть почти все) не тривиальны (хотя с точки зрения разговорной речи это может быть неожиданно). Вообще, «тривиальное» в строгом смысле == (как вариант) «терминальный объект в нужной категории». Помимо тривиальных алгебр ещё пример — unit type / тавтология ⊤ — тривиально населённый тип / тривиальная истина (arbitrary tautology) в категории типов / логических утверждений (всегда A → ⊤, если A ← ⊤, то A — населён / истина). Речь шла про доказательство 2 + 3 = 3 + 2. С применением (вычислительных) аксиом рассказывающих как обращаться с элементами множества ℕ с помощью операции _+_ получаем 5 = 5, которое истина в силу аксиомы рефлексивности отношения _=_, то есть ∀ x. x = x:

2 + 3 = 3 + 2
============= (def)
11 + 111 = 111 + 11
----------------------- (+1/+1)
1(1 + 111) = 1(11 + 11)
----------------------- (+1/+1)
11(0 + 111) = 11(1 + 11)
------------------------ (+0/+1)
11111 = 111(0 + 11)
------------------- (id/+0)
11111 = 11111
------------- (refl)
⊤

Считаем доказательства (дедукции) с помощью вычислительных аксиом и рефлексивности тривиальными — все остальные (не тривиальные, например ∀ a b. a + b = b + a) доказательства будут сводиться к ним. То есть я тут, фактически, объединяю объекты категории формул и дедукций в классы эквивалентности modulo вычисления и рефлексивность и у меня получается категория в которой {2 + 3 = 3 + 2, ..., ⊤} отождествлены в один терминальный объект «тривиально доказуемых» формул.

Да, я тоже хотел написать «математика». Самое поразительное - то, что я почти все понял. Но вообще, я знаю только пару основных понятий из теории категорий (как-то собирался посвятить ей больше времени, но нет мотивации, и учебника какого-то каноничного не нашел), поэтому рассуждения насчет категории формул и дедукций я чёт ниочинь. И пруф-ассистенты я тоже не тыкал палочкой в отсутствие надобности. Я даже не вижу четкой связи между теоремами, которые доказываются, и теоремами в смысле формальных систем, которые выводятся. Это одно и то же? Понятно, что привычные теоремы доказываются так же строго, не ведь для языка, на котором они формулируются, не существует правил вывода, чтоб на вход - аксиомы и правила, и на выходе бесконечно выплевываются теоремы?

Вот и я о том же, аксиомы - явно не продукционные правила. Скорее похожи на DTD.

Объясни, что означает «сформулировать аксиомами», для начала. А то я так думал, что формулируют обычно словами.

Не припутывай меня к своему онейроидному синдрому. Я никогда не говорил, что аксиомы - это не правила продукции, потому что это по определению совершенно разные объекты. Правила воздействуют на акисомы и их производные. В моем посте нет ни слова спора с тем, что ты подтверждаешь.

Ну вот скажем есть аксиома «целое больше части». Какие нетривиальные выводы из нее можно сделать?

поэтому рассуждения насчет категории формул и дедукций я чёт ниочинь

Это по Lambek-у (google://deductive+system+category — http://plato.stanford.edu/entries/category-theory, например). Из Mann «The connection between equivalence of proofs and Cartesian closed categories»:

there is in a cartesian closed category a terminal object, which must be represented by a formula in the formal system. The equivalence relation must allow for the fact that there is exactly one morphism into the terminal object from any other object. This terminal object is akin to a formula representing 'truth', which can be proved in essentially only one way.

про аксиомы как раз, такие как

------- (tt)
⊤ holds

----------- (refl)
x = x holds

То есть аксиомы — тривиальные теоремы, их доказательства — тривиальны, всё это терминальный объект и стрелки в него (там класс эквивалентности доказательств). Просто чтобы навести мосты с понятием «тривиально» из алгебры. Теперь из аксиом производим множество теорем исключительно «вычислительными» правилами вывода, суть в том, что такой вывод может быть однозначен и разрешим (Church–Rosser и нормализация), дальше добавляем весь класс таких теорем в класс очевидно-тривиальных аксиом, например

...
-------------------
2 + 3 = 3 + 2 holds

...
-------------------- (+0)
a |- 0 + a = a holds

...
--------------------------------------- (+1)
a, b |- (1 + a) + b = 1 + (a + b) holds

и считаем их тоже тривиальными. Это уже чтобы упростить доказательства «нетривиальных» вещей — современная теория типов (с учётом computational rules) и её реализации в пруф-ассистентах так делают — поэтому там 2 + 3 = 3 + 2 так же тривиально как и 5 = 5, вычислительное доказательство производится тайпчекером за ширмой, так же в случае 0 + a = a, (1 + a) + b = 1 + (a + b) и любых других распостранений бета-эквивалентностей задаваемых определениями функций.

Это одно и то же?

У Бурбаки есть такая сентенция:

Математик, желающий убедиться в полной правильности, или, как говорят, “строгости", доказательства или теории, отнюдь не прибегает к одной из тех полных формализаций, которыми мы сейчас располагаем, и даже большей частью не пользуется частичными и неполными формализациями, доставляемыми алгебраическим и другими подобными исчислениями. Обыкновенно он довольствуется тем, что приводит изложение к такому состоянию, когда его опыт и чутье математика говорят ему, что перевод на формализованный язык был бы теперь лишь упражнением в терпении. Если возникают сомнения, то, в конечном счете они относятся именно к возможности прийти без двусмысленности к такой формализации — употреблялось ли одно и то же слово в разных смыслах в зависимости от контекста, нарушались ли правила синтаксиса бессознательным употреблением способов рассуждения, не разрешаемых явно этими правилами, была ли, наконец, совершена фактическая ошибка. Текст редактируется, все больше и больше приближаясь к формализованному тексту, пока, по мнению специалистов, дальнейшее продолжение этой работы не станет излишним.

Правда в случае пруф-ассистентов остановиться уже нельзя — нужно формализировать до победного.

для языка, на котором они формулируются, не существует правил вывода, чтоб на вход - аксиомы и правила, и на выходе бесконечно выплевываются теоремы?

В смысле для естественного языка? Всё равно есть некоторое строгое представление о вещах в голове которые этим языком описываются — начиная с Евклида, плюс сейчас часто коммутативные и прочие диаграммы используются, явный equational reasoning, то есть когда вместо словесного описания выписываются шаги вывода и промежуточные результаты.

Ну вот скажем есть аксиома «целое больше части». Какие нетривиальные выводы из нее можно сделать?

Нет такой аксиомы.

Аксиомы — чистое описание тех фактов, существование которых имеется основание считать эмпирически доказанными

нет. Вот взять, например, аксиому выбора - ее можно принимать или не принимать. Получатся 2 разные математики.

У Евклида есть.

Что у Евклида? Аксиомы относятся к какой-то системе. К какой системе относится эта?

То, что мы называем «Аксиомой выбора», не является аксиомой.

Это является аксиомой по определению аксиомы - утверждение, не следующее из других аксиом и не входящее с ними в противоречие, которое мы в рассматриваемой ситуции принимаем за основу для дальнейшей теории (определение кривовато, но наглядно)

медианы не являются параллельными прямыми

они пересекаются

Возможно ли пользуясь только аксиомами сформулировать, скажем, теорему Пифагора? Не доказать, а именно открыть, сформулировать. А если нет, то какой тогда прок от таких оснований в деле накопления новых знаний?

сформулировать можно что угодно. Например, что сумма квадратов катетов равна всегда 7. Пользуясь аксиомами ты можешь это опровергнуть.

Сформулировать теорему Пифагора ты с помощью аксиом ИМХО не сможешь, но сможешь как-то иначе. К примеру сопоставив площади квадратов на катетах с квадратом на гипотенузе. Используя аксиомы ты можешь строго доказать свою догадку для всех таких случаев.

Олег Акимов утверждает, что знания не выводятся из каких-то принципов, а чуть ли не визуально конструируются исходя из жизненного опыта человека и его здравого смысла.

«принципы» == «здравый смысл». У нас аксиомы и так в мозгах вшиты, и называются «здравым смыслом». К примеру, если прямые не сходятся, и не расходятся, они никогда не сойдутся или не разойдутся. Это пятая аксиома. Ну или здравый смысл подсказывает, что все прямые углы одинаковы. Это четвёртая аксиома. И так далее.

Твоё утверждение содержит логическую ошибку.

Если аксиома не входит в противоречие с другими аксиомами, как же тогда понимать «теорему о неполноте», согласно которой всякая система математических аксиом (формальная система) начиная с определённого уровня сложности либо внутренне противоречива, либо неполна (то есть в достаточно сложных системах найдётся хотя бы одно высказывание, истинность и ложность которого не может быть доказана средствами самой этой системы)?

А какая тебе разница, если ты не понимаешь эту теорему?

Ну вот скажем есть аксиома «целое больше части». Какие нетривиальные выводы из нее можно сделать?

Нет такой аксиомы.

за то есть «часть не больше целого».

Нетривиальные выводы можно сделать потому, что из это аксиомы следует два случая:

1. часть равна целому, этот случай мы не рассматриваем, ибо он тривиален. Можно сказать, что в этом случае часть не является частью, а является целым.

2. часть меньше целого. Этот случай интересен тем, что его рекурсивное применение даёт нам возможность делить что угодно на любое целочисленное число. А также складывать что угодно, получая любые доли чего угодно.

Особенно полезен случай, когда обе части равны. Это позволяет ввести нам двоичную СС, которая позволяет за конечное и малое время выразить любое целое в любых единицах с точностью не хуже этой единицы.

Именно так и реализовано деление в современных компьютерах.

Т.о. мы придумали годный практический алгоритм. Тот же алгоритм позволяет найти не только частное, но и вообще что угодно и где угодно, необходимо и достаточно лишь уметь делить пополам где угодно, и выяснять, где прячется что угодно. И да, если пометить оба результата например левая часть 0, а правая часть 1, и запоминать эти биты к примеру при делении пустыни со львом, и прекратить деление как только делить придётся льва, то расстояние от левого края до льва будет выражено двоичным числом, в единицах равных льву.

ни в одной из геометрий нет [различных]параллельных прямых которые имеют хотя бы одну общую точку.

медианы являются параллельными. Причина проста: они не сходятся. Это можно доказать: если опустить перпендикуляр от одной медианы, но пересечёт другую медиану под прямым углом. Следовательно, медианы НЕ сходятся, т.к. их направление одинаково. Меридианы пересекаются не потому-что они в разных направлениях идут, а просто потому, что НЕ являются прямыми на плоскости. Вот они и сходятся в одно точке кривой «плоскости». По этой-же причине сумма углов любого треугольника >180 градусов — стороны не являются прямыми, радиус кривизны положительный, и треугольник пучит. Вот и углы получаются больше. Если задумать построить самый большой треугольник, углы его ВНЕЗАПНО делятся на ноль. «Треугольник» становится экватором, у которого тупо нет углов. Такие свойства имеет любая поверхность в точках, где радиус кривизны положителен.

если вы бездоказательно (т.е аксиома это для вас) утверждаете что «существует геометрия в которых параллельные_друг_другу_прямые не параллельны_друг_другу»

параллельные параллельны, что не мешает им сходится в некоторых точках. Что в этом странного?

медианы являются параллельными.

https://upload.wikimedia.org/wikipedia/commons/5/5e/Triangle.Centroid.svg?use...

пусть геометрия нашего 3мерия имеет положительную? кривизну - тогда не существует параллельных прямых в нём

это неправильно. Если определить параллельные прямые как прямые с одним направлением, то это не так. Пересечём два меридиана любой прямой, и сравним углы. Если углы одинаковые значи прямые идут в одном направлении. И никогда не встретятся на нормальной плоскости (с нулевой кривизной). Но на НЕ НОРМАЛЬНОЙ «плоскости» могут встретится, если сама плоскость свернётся в точку. Именно так, как делает сфера. Прямые сначала сходятся на полюсе шара, а потом расходятся по мнимой поверхности шара, которой нет (шар-то уже кончился).

блин, я про меридианы, а не про медианы ессно.

Конкретно теорема Пифагора была открыта до открытия аксиом

это было просто наблюдение без доказательств. Ничем не лучше наблюдения «Б-г есть».

а чуть ли не визуально конструируются исходя из жизненного опыта человека и его здравого смысла.

На высоких уровнях знания то и другое сосет с причмоком.

нет. Это так лишь если ты потребляешь чужие знания и принимаешь их на веру(пусть даже вызубрив формальное доказательство). Если ты _действительно_ осилил доказательство, твой опыт и здравый смысл изменяется, а именно инкрементируется. На высоких уровнях у теяб опыт и здравый смысл Over9000, потому тебе очевидны даже сложные вещи. К примеру даже с моим 80м lvl матана, мне очевидно, что параллельные прямые пересекаются на кривой плоскости. А для кого-то это разрыв моска.

получаем 5 = 5, которое истина в силу аксиомы рефлексивности отношения _=_, то есть ∀ x. x = x:

У тебя тут ошибка. X не может быть любым. Если X не определено, то и истинность выражения X=X тоже не определена. Т.е. твоё следует понимать не как «любое», а любое заведомо определенное x. Т.е. что-бы быть истинным, равенству X=X требуется определённость X, что вообще говоря ты не постулировал. И эта внутренняя противоречивость обязательно потом вылезет.

Логический капкан захлопнулся в тот момент, когда ты написал ∀. Для полноты твоей алгебры любое действие должно иметь обратную операцию, а вот твое ∀ принципиально односторонне, и обратного пути нет. Это не просто невозможно, но и не имеет никакого смысла. Именно этот капкан подстерегает тебя когда ты пишешь ∀*0=0, откуда прямо следует деление на ноль и разыменовывание ∀.

Раз в твоей алгебре определено соотношение X=X, и наверное X+Y, то твоя алгебра определяет и ноль. А ещё умножение. И деление на ноль. Но деление на ноль приводит к разименованию ∀, а это не имеет смысла.

ЧиТД. Вся твоя алгебра не имеет смысла.

ЗЫЖ опасайся НЁХ.

То, что мы называем «Аксиомой выбора», не является аксиомой.

Аксиома это формула, ∀ A B. ∀ f : A ↠ B. ∃ g : B → A. f ∘ g = id(B) — вполне формула (можно ещё раскрыть ↠ и ∘ с id).

Аксиома, или знание абсолютное, – это утверждение, в рамках данной логической схемы исключающее противоположное по смыслу (альтернативное) и в принципе не допускающее возможности опровержения каким бы то ни было опытом.
А математическая формула — это принятая в математике (а также физике и прикладных науках) символическая запись законченного логического суждения (определения величины, уравнения, неравенства или тождества).

http://en.wikipedia.org/wiki/Binary_relation

A binary relation R is usually defined as an ordered triple (X, Y, G) where X and Y are arbitrary sets (or classes), and G is a subset of the Cartesian product X × Y.

http://en.wikipedia.org/wiki/Structure_(mathematical_logic)#Domain

http://en.wikipedia.org/wiki/Model_theory#First-order_logic

http://www.math.psu.edu/simpson/notes/master.pdf

алгебра

http://en.wikipedia.org/wiki/Signature_(logic)#Definition

a signature with no relation symbols is called an algebraic signature.

Здравый смысл не может быть у каждого своим. Это медиана. Вот Иванову Сидору Петровичу совершенно очевидно, что инопланетяне облучают его посредством кастрюли Софьи Николаевны. И какой же это здравый смысл?

А интуитивизм (http://ru.wikipedia.org/wiki/интуитивизм) - очень спорная штука.

Многие ссылаются вот на эту книженцию, вроде толковая - Асмус В.Ф. Проблемы интуиции в философии и математике. М., 1963;

http://ru.wikipedia.org/wiki/Интуиционизм

Судя по вики интуитивная логика сосет, так как не удовлетворяет тезису Чёрча, принципу Маркова, закону двойного отрицания и закону исключенного третьего.

У Евклида есть.

Вот к нему тогда и вопросы.

Серьёзно, ну, со времён Евклида ведь много чего произошло. «Начала» не актуальны ни насколько.

за то есть «часть не больше целого».

Нет.

Ну вот скажем есть аксиома «целое больше части».

Подели бесконечность пополам. То-то.

К примеру даже с моим 80м lvl матана, мне очевидно, что параллельные прямые пересекаются на кривой плоскости.

Видимо, уровень матана 80-й только по модулю. А со знаком там хреново.

http://en.wikipedia.org/wiki/Parallel_(geometry) — «In a non-Euclidean space, parallel lines are those that intersect only in the limit at infinity.»

Серьёзно, ну, со времён Евклида ведь много чего произошло.

Причем настолько, что практически все уверены что аксиоматика геометрии была сразу дана в том виде, в котором изложена у Погорелова.

это было просто наблюдение без доказательств. Ничем не лучше наблюдения «Б-г есть».

Вот чтобы не было такого впечатления и нужно регулярно кормить математиков сырыми данными.

Причем настолько, что практически все уверены что аксиоматика геометрии была сразу дана в том виде, в котором изложена у Погорелова.

Погорелов — это кто?

Диваноперидолу срочно :)

Каким ещё опытом и что если теория противоречива — почему бы не иметь доказательство утверждения противоположного по смыслу аксиоме.

В формальной логике аксиома теории это постулируемая от балды сентенция-формула которая должна быть истинна во всех моделях теории. А формула в FOL/HOL это просто формула — тоже есть определение.

Даже не знаю — выше была ссылка http://www.math.psu.edu/simpson/notes/master.pdf, до того места где приводятся сентенции представляющие собой аксиомы теории (!) групп. Хотя точного определения аксиомы там нет, так что http://ncatlab.org/nlab/show/axiom, http://ncatlab.org/nlab/show/theory#SyntacticView — тут есть ссылка на книжку, тоже самое в Sheaves in geometry and logic.

Наверно должен быть какой-то классический текст по математической логике или теории моделей в котором всё это простым языком объясняется. Точная ссылка на википедию это http://en.wikipedia.org/wiki/Axiom#Non-logical_axioms, в качестве источника там Mendelson, ещё, думаю, у Чёрча, Клини и Карри всё есть (есть переведённые учебники).