https://studopedia.su/14_161201_vivodimost-i-dokazuemost-formul.html

"доказуемая формула" == "теорема"

«Формула из А языка α , выводимая в исчислении α из пустого множества формул, называется доказуемой формулой, или теоремой исчисления α, а сам вывод формулы А из пустого множества формул называется ее доказательством.»
   (что такое "исчисление"? зачем здесь "язык"?)

"доказательство" == "вывод"

«Выводом формулы А из конечного или бесконечного множества формул Т в исчислении α
называется конечная последовательность формул А1, А2, …, An, в которой An = A
и каждая из формул Ai, i = 1, …, n является
- или аксиомой
- или формулой из Т (исходной формулой)
- или получается по некоторому правилу вывода из предыдущих формул этой последовательности
   (что такое "правило вывода"? какие бывают правила вывода? бывают ли правила вывода для "женской логики"?)

Если существует вывод формулы А из множества формул Т исчисления α, то говорят, что в α А выводима из Т и пишут
Т_α ├─_α А, или В1, В2, …, ВК ├─ А,

если Т = {В1, В2, …, ВК}. При этом формулы из Т называют посылками вывода.
Особо важным является случай, когда Т — пустое множество.»
    (другими словами, особый случай, это когда теорема выводится только из аксиом)

Формула из А языка α , выводимая в исчислении α из пустого множества формул, называется доказуемой формулой, или теоремой исчисления α, а сам вывод формулы А из пустого множества формул называется ее доказательством. Если формула А доказуема в исчислении α, то пишут

├─_α А.

   (то есть выводимость может быть из ещё недоказанных предпосылок, а доказуемость - это выводимость из аксиом)

https://fil.wikireading.ru/29 - текст непонятный, трэшовый, мусорный, для помойки.

Отредактировано Лис (2019-11-24 17:15:18)