|
Исчисление высказываний - наиболее простой пример формальной аксиоматической теории в логике. Существует несколько исчислений высказываний (Д. Гильберта, С. Клини, Ж. Фреге, П.С. Новикова). Мы рассмотрим исчисление высказываний Я. Лукасевича (исчисление ), использующее функционально полную систему связок, состоящую из отрицания ( ) и импликации ( ). Исчисление описывает множество тождественно истинных формул (тавтологий), что соответствует реальному положению вещей в математике, где теоремы как высказывания являются тождественно истинными формулами.
Язык исчисления включает перечень употребляемых символов и определение понятия формулы. Символами исчисления являются (счётное) множество символов пропозициональных (логических) переменных символы логических операций отрицания и импликации , а также вспомогательные символы скобок ( , ). Знаки других логических операций рассматриваются здесь как обозначения формул исчисления , выражающих эти операции (например, формулу можно считать обозначением эквивалентной ей формулы , построенной с помощью лишь отрицания и импликации). Понятие формулы исчисления определяется индуктивно: формулами полагаются сначала переменные а затем все выражения вида и , где в качестве и могут выступать любые из уже имеющихся формул.
Систему аксиом исчисления составляет бесконечное (счетное) множество формул исчисления, построенных с использованием следующих трех схем аксиом:
Аксиомой считается каждая формула, полученная подстановкой в схему аксиом любых формул исчисления вместо переменных .
Правилом вывода в исчислении является modus ponens (правило заключения), согласно которому из данных формул вида и выводится формула .
Исчисление предикатов первого порядка и теории первого порядка. Предикат - это логическая функция от нелогических аргументов (например, функция sum(x,y,z) принимает истинные значения, когда x+y=z, и ложные - в противном случае). Исчисление предикатов первого порядка и теории первого порядка отличаются от теорий более высоких порядков тем, что в них допускается применение кванторов только лишь к переменным. Однако установлено, что большинство теорий более высоких порядков сводимо к теориям первого порядка. Каждая теория первого порядка располагает системой аксиом, включающей логические (общие) и собственные (частные) аксиомы. Исчисление предикатов первого порядка - это теория первого порядка, использующая только логические аксиомы. Дополнение исчисления предикатов аксиомами некоторой предметной области превращает его в частную теорию первого порядка этой предметной области.
Исчисление предикатов первого порядка является определенным расширением исчисления высказываний, поэтому на основе каждого исчисления высказываний может быть построено соответствующее ему исчисление предикатов. Здесь будет рассматриваться исчисление предикатов (ИП), включающее систему связок и аксиом исчисления высказываний Лукасевича. Большинство обсуждаемых здесь результатов (кроме особо оговоренных для ИП) относится к любым теориям первого порядка.
Язык теорий первого порядка богаче языка исчисления высказываний благодаря использованию (нелогических) предметных переменных, что влечет за собой необходимость рассмотрения логических и нелогических функций от нелогических переменных (наряду с логическими переменными и логическими связками исчисления высказываний). По этой причине множество символов теорий первого порядка включает подмножества:
- символов предметных констант;
- функциональных символов (функторов);
- предикатных символов (предикатов);
- символов предметных переменных;
- логических символов;
- вспомогательных символов.
Множество символов называется сигнатурой. Символы, входящие в сигнатуру, выделены в особое подмножество по той причине, что наделение этих символов предметным содержанием связывает формальную аксиоматическую теорию с конкретной предметной областью (формальная аксиоматическая теория получает предметную интерпретацию), благодаря чему одна и та же формальная аксиоматическая теория оказывается применимой в различных предметных областях.
Do'stlaringiz bilan baham: |
