Как называется утверждение, которое принимается за истинное, но никогда не было доказано?

Как вы назовете утверждение P , которое никогда не было формально доказано, но все наблюдения подтверждают его?

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

В этом примере P — это утверждение « эта функция не содержит ошибок ».

Гипотеза. См. гипотезу Ферма до 1994 г.
Неформально это можно было бы назвать «возможностью».
Непонятно, о чем вы спрашиваете сейчас, после вашего редактирования. Утверждение «это всегда работало, даже если мы не знаем, как это сделать» просто верно (верю вам на слово). Итак, какое утверждение вы имеете в виду, когда говорите «утверждение, которое никогда не было доказано»? Вы хотите спросить: как мы называем ситуацию, в которой мы не знаем, как что-то работает?
@EliranH Альберто описывает индукцию. «Мы не знаем наверняка, будет ли программа продолжать работать, потому что мы не можем доказать, что она будет работать, но она всегда работала в прошлом, поэтому мы думаем, что она продолжит работать». Недоказанное утверждение состоит в том, что он будет продолжать работать .
Что означает «эта функциональность»? Вы имеете в виду "эту программу"? Доказательство касается предложений/программ, а не функциональности.
@mobileink Извините, я пишу «функциональность», но я хочу написать «функция» (программа — это функция).
Ах, но программы на самом деле не функции, это процедуры, которые представляют или приближают fns. Доказательство программы, функциональной или нет, связано с реализацией, которая представляет собой конкретный текст. Извините за придирчивость, но это хороший вопрос, который затрагивает множество вещей, поэтому чем точнее мы сможем ответить, тем лучше.
предложение: "Реализация этой функции безошибочна". У данного fn может быть много реализаций.

Ответы (6)

Частично это зависит от предметной области, в которую попадает утверждение, и от того, насколько оно было подтверждено фактами (например, просто еще не опровергнутым или тщательно проверенным и подтвержденным). Создание комментариев:

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

В науке это назвали бы гипотезой .

Более общим термином была бы [эпистемическая] возможность . Обратите внимание, что это эпистемическое, потому что мы говорим о доказательствах и способах, которыми мы можем узнать, что что-то истинно; модальность не очень актуальна.

Отредактировано после вопроса:

Ваш пример интересен, потому что он не совсем соответствует предложенным терминам. Я бы сказал, что это более общий случай индуктивного утверждения («Это всегда работало в прошлом, поэтому оно будет работать и дальше»). Вывод о том, что он продолжит работать, можно назвать индукцией . Это соответствует образцу обращения к дедуцируемому заключению как к дедукции .

Сократ мудр, а Сократ человек. Мой вывод состоит в том, что некоторые люди мудры.

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

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

Спасибо за ответ. Смотрите мои правки, если вам нужны разъяснения.
@ Альберто Я отредактировал свой ответ с другим предложением.
Спасибо @Era, пример яблока — это именно то, что я пытался сказать. Я думаю, что индукция подходит для моего случая.
Спасибо, @Era, я обнаружил, что "гипотеза" - правильное слово.

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

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

Конечно, эта функциональность правильная, потому что она никогда не подводила.

Это неверный вывод. То, что он еще не потерпел неудачу, не означает, что этого не произойдет в будущем. Мы не можем быть уверены.

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

Для конкретной ситуации с программным обеспечением, которую вы описываете, взгляните на Hoare Logic, как обсуждалось, например, в https://en.wikipedia.org/wiki/Hoare_logic .

В этой модели корректность вашей программы определяется набором троек Хоара в форме {P}C{Q} , где {P} = предусловия/ввод, C = ваша_программа, {Q} = постусловия/вывод. Учитывая ввод, удовлетворяющий любому из предписанных предварительных условий, если вывод вашей программы удовлетворяет соответствующим постусловиям, то он «правильный».

В качестве простого примера предположим, что C =program_to_add_two_numbers. Тогда одна тройка Хоара может быть {P}C{Q} , где {P} =both_numbers_to_be_added_are_нечетно, а {Q} =sum_is_even. Очевидно, что одна тройка Хоара сама по себе не устанавливает правильность C. Но подходящая коллекция троек Хоара обычно помогает. («Обычно» означает всякий раз, когда существует набор троек Хоара, который однозначно, в смысле «если и только если», определяет функцию : ввод -> вывод, которую необходимо вычислить.)

И вы можете проверить некоторые из ссылок «См. также» в нижней части этой статьи в Википедии, чтобы узнать о нескольких других моделях корректности программ. Как вы можете себе представить, компьютерная наука посвятила этому предмету множество тщательных исследований.

edit: Спасибо, @JamesKingsbery Что касается вашего замечания «термин для этой концепции», да, я должен был прямо упомянуть, что вы можете найти в Google термин «корректность программы» для получения большого количества дополнительной информации.

Добро пожаловать в Философия.SE! Отличный ответ на вопрос, я не знал, что для этого понятия есть термин!

Насколько я понимаю стандартное использование, формально доказуемое предложение является теоремой, поэтому «P является теоремой» говорит, что P истинно и что утверждение, что P истинно, подтверждается дедуктивным доказательством. Гипотеза выдвигается как верная, но без формального обоснования, будь то дедуктивного или индуктивного. Эмпирические утверждения никогда не доказуемы формально, поэтому их обоснования бывают либо индуктивными, либо абдуктивными. Это верно даже для «законов»; например, Закон Ома нельзя доказать формально. Лучшее, что мы можем сделать, это провести множество экспериментов, заметить, что оно никогда не нарушается, и сделать вывод (индуктивно? абдуктивно?), что это должно быть правдой. Тогда мы называем это теорией (о мире природы).

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

Я бы предложил опираться на инженерию, а не на логику, и назвать такие программы надежными . Это имеет то преимущество, что устраняет понятие истины, которое является философским вопросом, не имеющим отношения к технике. У него также есть хорошее формальное статистическое определение, которым я не буду вас утомлять, и оно связано с такими понятиями, как надежность, поскольку обоснование заявлений о надежности будет включать дисперсию: если ваш код работает в течение 10 лет без ошибок, но всегда с один и тот же вход, то он может быть надежным для этого входа, но вы понятия не имеете, насколько он надежен, т.е. надежен ли он в различных условиях.

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

В частности, в отношении программ/функций это совершенно другое дело. Программа создается человеком (-ами), поэтому будет ли программа работать «всегда» во «всех возможных» условиях, зависит от того, насколько тщательно программист предусмотрел все такие возможные ошибки и насколько тщательно отдел тестирования выполнил свою работу. . Очевидно, что чем тщательнее были проведены эти мероприятия, тем меньше вероятность того, что программа провалится. Однако высокая вероятность «человеческих ошибок» не позволяет гарантировать , что та или иная программа (или функция) всегда будет работать при любых условиях! Следовательно, утверждению «эта функция не содержит ошибок» должно предшествовать выражение «пока что,this...", чтобы сделать его "разумным" утверждением (утверждением, имеющим смысл).

Утверждение, которое принимается за истину, но никогда не было доказано? В математике вы бы назвали это «неверно принятым за истину».

Даже в разработке программного обеспечения, где стандарты будут ниже, никто в здравом уме никогда не назовет какое-либо программное обеспечение «безошибочным». Вы можете услышать, что в программном обеспечении нет известных ошибок или дефектов.